fix(frontends/lean): missing type info in expressions nested in tactics

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();
         }

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

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