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

fix(library/blast/blast): update local2lref

Browse source
This commit is contained in:
Leonardo de Moura 2015-09-29 09:30:58 -07:00
parent 459f31f28b
commit 9622b62537
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/blast/blast.cpp
View file

@ -192,7 +192,8 @@ class context {
for (expr const & h : hs) { for (expr const & h : hs) {
lean_assert(is_local(h)); lean_assert(is_local(h));
expr new_type = to_blast_expr(mlocal_type(h)); expr new_type = to_blast_expr(mlocal_type(h));
s.add_hypothesis(local_pp_name(h), new_type, none_expr(), some_expr(h)); expr lref = s.add_hypothesis(local_pp_name(h), new_type, none_expr(), some_expr(h));
local2lref.insert(mlocal_name(h), lref);
} }
expr new_target = to_blast_expr(g.get_type()); expr new_target = to_blast_expr(g.get_type());
s.set_target(new_target); s.set_target(new_target);