From 9622b625377a79b42f715b3f1930e37b29c65bb0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 29 Sep 2015 09:30:58 -0700 Subject: [PATCH] fix(library/blast/blast): update local2lref --- src/library/blast/blast.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index af566377e..618695948 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -192,7 +192,8 @@ class context { for (expr const & h : hs) { lean_assert(is_local(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()); s.set_target(new_target);