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

fix(kernel/metavar): improve error messages by propagating the tag when we execute instantiate_all

Browse source 
This is the real fix for commit ededf4fc6c
This commit is contained in:
Leonardo de Moura 2015-03-02 13:01:50 -08:00
parent c81762970e
commit 1042bbc06f
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/kernel/metavar.cpp
View file

@ -185,7 +185,7 @@ protected:
if (!modified) if (!modified)
return e; return e;
else else
return mk_rev_app(new_f, new_args); return mk_rev_app(new_f, new_args, e.get_tag());
} }
expr save_result(expr const & e, expr && r) { expr save_result(expr const & e, expr && r) {