michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/tactic/rewrite_tactic): matcher should unfold only reducible constants

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-06 13:44:04 -08:00
parent b4139627e5
commit 5b2a9dacc2
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/tactic/rewrite_tactic.cpp
View file

@ -1026,7 +1026,7 @@ class rewrite_fn {
public: public:
rewrite_fn(environment const & env, io_state const & ios, elaborate_fn const & elab, proof_state const & ps): 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_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_matcher_tc(mk_matcher_tc()),
m_mplugin(m_ios, *m_matcher_tc) { m_mplugin(m_ios, *m_matcher_tc) {
goals const & gs = m_ps.get_goals(); goals const & gs = m_ps.get_goals();