From cd144993c031ce8d6eb1b5fd581c7a7f4041e73a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Oct 2015 16:30:37 -0700 Subject: [PATCH] chore(frontends/lean/prenum,library/tactic/rewrite_tactic): fix style --- src/frontends/lean/prenum.cpp | 1 + src/library/tactic/rewrite_tactic.cpp | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/frontends/lean/prenum.cpp b/src/frontends/lean/prenum.cpp index 693442967..417671c46 100644 --- a/src/frontends/lean/prenum.cpp +++ b/src/frontends/lean/prenum.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include "library/kernel_serializer.h" namespace lean { diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index 8c6f4d6a5..82fb5a493 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -1598,7 +1598,7 @@ class rewrite_fn { type_checker_ptr mk_tc(bool full) { auto aux_pred = full ? mk_irreducible_pred(m_env) : mk_not_quasireducible_pred(m_env); - return mk_type_checker(m_env, m_ngen.mk_child(),[=](name const & n) { + return mk_type_checker(m_env, m_ngen.mk_child(), [=](name const & n) { return aux_pred(n) && !is_numeral_const_name(n); }); }