From 666f697d24850bb176ac4751b6b44d0fe72e1910 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 8 Feb 2015 17:27:22 -0800
Subject: [PATCH] fix(frontends/lean/builtin_exprs): 'using' expression should
 make local constant available for tactics

---
 src/frontends/lean/builtin_exprs.cpp | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 0dfd72b1c..eeba1a6d8 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -233,21 +233,28 @@ static expr parse_proof(parser & p, expr const & prop) {
         p.next();
         parser::local_scope scope(p);
         buffer<expr> locals;
+        buffer<expr> new_locals;
         while (!p.curr_is_token(get_comma_tk())) {
             auto id_pos = p.pos();
             expr l      = p.parse_expr();
             if (!is_local(l))
                 throw parser_error("invalid 'using' declaration for 'have', local expected", id_pos);
-            p.add_local(l);
+            expr new_l = l;
+            binder_info bi = local_info(l);
+            if (!bi.is_contextual())
+                new_l = update_local(l, bi.update_contextual(true));
+            p.add_local(new_l);
             locals.push_back(l);
+            new_locals.push_back(new_l);
         }
         p.next(); // consume ','
         expr pr = parse_proof(p, prop);
         unsigned i = locals.size();
         while (i > 0) {
             --i;
-            expr l = locals[i];
-            pr = p.save_pos(Fun(l, pr), using_pos);
+            expr l     = locals[i];
+            expr new_l = new_locals[i];
+            pr = p.save_pos(Fun(new_l, pr), using_pos);
             pr = p.save_pos(mk_app(pr, l), using_pos);
         }
         return pr;