From f027acb5cb49c372fd0ac9e91b7201e4c8ff125a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 23 Oct 2014 18:31:05 -0700
Subject: [PATCH] fix(frontends/lean): missing type info in expressions nested
 in tactics

---
 src/frontends/lean/elaborator.cpp             |  8 +++--
 tests/lean/interactive/apply_info.input       | 22 ++++++++++++
 .../interactive/apply_info.input.expected.out | 36 +++++++++++++++++++
 3 files changed, 63 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/interactive/apply_info.input
 create mode 100644 tests/lean/interactive/apply_info.input.expected.out

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 2e5950ba9..b2d14a51a 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1144,7 +1144,7 @@ static expr translate_local_name(environment const & env, list<expr> const & ctx
                                  expr const & src) {
     for (expr const & local : ctx) {
         if (local_pp_name(local) == local_name)
-            return local;
+            return copy(local);
     }
     // TODO(Leo): we should create an elaborator exception.
     // Using kernel_exception here is just a dirty hack.
@@ -1161,12 +1161,14 @@ static expr translate(environment const & env, list<expr> const & ctx, expr cons
             return some_expr(e); // ignore placeholders
         } else if (is_constant(e)) {
             if (!env.find(const_name(e))) {
-                return some_expr(translate_local_name(env, ctx, const_name(e), e));
+                expr new_e = copy_tag(e, translate_local_name(env, ctx, const_name(e), e));
+                return some_expr(new_e);
             } else {
                 return none_expr();
             }
         } else if (is_local(e)) {
-            return some_expr(translate_local_name(env, ctx, local_pp_name(e), e));
+            expr new_e = copy_tag(e, translate_local_name(env, ctx, local_pp_name(e), e));
+            return some_expr(new_e);
         } else {
             return none_expr();
         }
diff --git a/tests/lean/interactive/apply_info.input b/tests/lean/interactive/apply_info.input
new file mode 100644
index 000000000..9128fd174
--- /dev/null
+++ b/tests/lean/interactive/apply_info.input
@@ -0,0 +1,22 @@
+VISIT apply_info.lean
+SYNC 17
+import logic
+theorem tst1 (a b : Prop) : a → b → a ∧ b :=
+begin
+ intro Ha,
+ intro Hb,
+ apply and.intro,
+ apply Ha,
+ apply Hb,
+end
+
+theorem tst2 (a b : Prop) : a → b → a ∧ b :=
+assume Ha Hb,
+begin
+ apply and.intro,
+ apply Ha,
+ apply Hb,
+end
+WAIT
+INFO 7
+INFO 16
\ No newline at end of file
diff --git a/tests/lean/interactive/apply_info.input.expected.out b/tests/lean/interactive/apply_info.input.expected.out
new file mode 100644
index 000000000..886451aa6
--- /dev/null
+++ b/tests/lean/interactive/apply_info.input.expected.out
@@ -0,0 +1,36 @@
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGININFO
+-- TYPE|7|1
+tactic.expr → tactic
+-- ACK
+-- IDENTIFIER|7|1
+tactic.apply
+-- ACK
+-- TYPE|7|7
+a
+-- ACK
+-- IDENTIFIER|7|7
+Ha
+-- ACK
+-- TYPE|7|9
+tactic
+-- ACK
+-- ENDINFO
+-- BEGININFO
+-- TYPE|16|1
+tactic.expr → tactic
+-- ACK
+-- IDENTIFIER|16|1
+tactic.apply
+-- ACK
+-- TYPE|16|7
+b
+-- ACK
+-- IDENTIFIER|16|7
+Hb
+-- ACK
+-- TYPE|16|9
+tactic
+-- ACK
+-- ENDINFO