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

fix(frontends/lean/elaborator): propagate tags for getting better error messages

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-13 11:10:26 +01:00
parent 8da44f1cd5
commit 1d16b5d2ad
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/elaborator.cpp
View file

@ -295,10 +295,10 @@ class elaborator {
continue;
expr type = decl->get_type();
// create the term pre (inst _ ... _)
expr pre = copy_tag(m_mvar, mk_explicit(mk_constant(inst)));
expr pre = copy_tag(m_mvar, mk_explicit(copy_tag(m_mvar, mk_constant(inst))));
while (is_pi(type)) {
type = binding_body(type);
pre = copy_tag(m_mvar, ::lean::mk_app(pre, mk_expr_placeholder()));
pre = copy_tag(m_mvar, ::lean::mk_app(pre, copy_tag(m_mvar, mk_expr_placeholder())));
}
try {
scope s(m_elab, m_ctx, m_subst);