From c49f51dccc8e12aa30aefcc31ed3c2bb5250121f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 8 Jul 2016 21:53:33 -0700 Subject: [PATCH] perf(library/tactic/simplifier/simplifier): minimize number of check_system invocations --- src/library/tactic/simplifier/simplifier.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/tactic/simplifier/simplifier.cpp b/src/library/tactic/simplifier/simplifier.cpp index 84df85dd0c..3e7a239cc4 100644 --- a/src/library/tactic/simplifier/simplifier.cpp +++ b/src/library/tactic/simplifier/simplifier.cpp @@ -305,7 +305,6 @@ expr simplifier::whnf_eta(expr const & e) { /* Simplification */ simp_result simplifier::simplify(expr const & e) { - check_system("simplifier"); m_num_steps++; lean_trace_inc_depth("simplifier"); lean_trace_d("simplifier", tout() << m_rel << ": " << e << "\n";); @@ -350,6 +349,7 @@ simp_result simplifier::simplify(expr const & e) { r = join(r, simplify_pi(r.get_new())); break; case expr_kind::App: + check_system("simplifier"); r = join(r, simplify_app(r.get_new())); break; case expr_kind::Let: