From 8926e98090189c2e810709db6d96f810f4452d1b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 8 Feb 2017 23:14:43 -0800 Subject: [PATCH] fix(library/tactic/simplify): missing constraints This bug was introduced in the previous commit. --- src/library/tactic/simplify.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp index a4b45ffcc0..35a3ae7945 100644 --- a/src/library/tactic/simplify.cpp +++ b/src/library/tactic/simplify.cpp @@ -498,8 +498,8 @@ simp_result simplify_core_fn::rewrite(expr const & e) { } struct match_fn { - tmp_type_context & m_ctx; - name const & m_id; + tmp_type_context & m_ctx; + name const & m_id; buffer> m_postponed; match_fn(tmp_type_context & ctx, name const & id):m_ctx(ctx), m_id(id) {} @@ -538,9 +538,9 @@ struct match_fn { bool operator()(expr const & p, expr const & t) { if (!match(p, t)) return false; - for (auto const & e : m_postponed) { + for (unsigned i = 0; i < m_postponed.size(); i++) { expr p1, t1; bool implicit; - std::tie(p1, t1, implicit) = e; + std::tie(p1, t1, implicit) = m_postponed[i]; p1 = m_ctx.instantiate_mvars(p1); if (implicit) p1 = m_ctx.ctx().complete_instance(p1); @@ -575,7 +575,7 @@ simp_result simplify_core_fn::rewrite_core(expr const & e, simp_lemma const & sl if (!instantiate_emetas(tmp_ctx, sl.get_num_emeta(), sl.get_emetas(), sl.get_instances())) { lean_trace_d(name({"debug", "simplify", "try_rewrite"}), tout() << "fail to instantiate emetas: " << - sl.get_id() << "\n";); + sl.get_id() << "\n" << e << "\n";); return simp_result(e); }