From 5b2a9dacc25cb7a72d71145157481134fdea211b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 6 Feb 2015 13:44:04 -0800 Subject: [PATCH] fix(library/tactic/rewrite_tactic): matcher should unfold only reducible constants --- src/library/tactic/rewrite_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index 54c793128..bc8550386 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -1026,7 +1026,7 @@ class rewrite_fn { public: rewrite_fn(environment const & env, io_state const & ios, elaborate_fn const & elab, proof_state const & ps): m_env(env), m_ios(ios), m_elab(elab), m_ps(ps), m_ngen(ps.get_ngen()), - m_tc(mk_type_checker(m_env, m_ngen.mk_child(), ps.relax_main_opaque())), + m_tc(mk_type_checker(m_env, m_ngen.mk_child(), ps.relax_main_opaque(), OpaqueIfNotReducibleOn)), m_matcher_tc(mk_matcher_tc()), m_mplugin(m_ios, *m_matcher_tc) { goals const & gs = m_ps.get_goals();