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

fix(frontends/lean/proof_qed_elaborator): must also create

Browse source 
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.
This commit is contained in:
Leonardo de Moura 2014-09-25 20:07:51 -07:00
parent c775da16ec
commit d02ab15c88
1 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/frontends/lean/proof_qed_elaborator.cpp
View file

@ -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<constraint> 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);
};