From d02ab15c889886c8bdc22d7cb997d07d26d82e05 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 25 Sep 2014 20:07:51 -0700 Subject: [PATCH] fix(frontends/lean/proof_qed_elaborator): must also create metavar_closure before solving nested proof_qed The bug was exposed by the new policy for handling class-instance resolution. In the new policy, we reject partial solutions. The bug fixed in this commit was being masked by a partial solution that was being "completed" later. --- src/frontends/lean/proof_qed_elaborator.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/proof_qed_elaborator.cpp b/src/frontends/lean/proof_qed_elaborator.cpp index 7d9fcf2c27..5a739439e4 100644 --- a/src/frontends/lean/proof_qed_elaborator.cpp +++ b/src/frontends/lean/proof_qed_elaborator.cpp @@ -28,7 +28,12 @@ constraint mk_proof_qed_cnstr(environment const & env, expr const & m, expr cons constraint_seq new_cs = cs + tcs.second + dcs.second; buffer cs_buffer; new_cs.linearize(cs_buffer); + + metavar_closure cls(meta); + cls.add(meta_type); + cls.mk_constraints(s, j, relax, cs_buffer); cs_buffer.push_back(mk_eq_cnstr(meta, e, j, relax)); + unifier_config new_cfg(cfg); new_cfg.m_discard = false; unify_result_seq seq = unify(env, cs_buffer.size(), cs_buffer.data(), ngen, new_cfg); @@ -40,8 +45,6 @@ constraint mk_proof_qed_cnstr(environment const & env, expr const & m, expr cons // we erase internal justifications return update_justification(c, j); }); - metavar_closure cls(meta); - cls.add(meta_type); constraints r = cls.mk_constraints(new_s, j, relax); return append(r, postponed); };