From ededf4fc6c63b0dd21268ca2a10cd982ae52174b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 1 Mar 2015 14:51:44 -0800
Subject: [PATCH] feat(frontends/lean): remove unnecessary instantiate_all's
 that were messing with error localization

---
 src/frontends/lean/elaborator.cpp            |  4 ++--
 src/library/tactic/elaborate.cpp             |  2 +-
 tests/lean/change_tac_fail.lean              | 12 ++++++++++++
 tests/lean/change_tac_fail.lean.expected.out |  8 ++++++++
 4 files changed, 23 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/change_tac_fail.lean
 create mode 100644 tests/lean/change_tac_fail.lean.expected.out

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index a4adb7f96b..3c933b306f 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1586,7 +1586,7 @@ bool elaborator::try_using_begin_end(substitution & subst, expr const & mvar, pr
                 return false;
             ps = proof_state(ps, tail(gs), subst, ngen);
         } else {
-            expr new_ptac = subst.instantiate_all(ptac);
+            expr new_ptac = ptac;
             if (auto tac = pre_tactic_to_tactic(new_ptac)) {
                 try {
                     proof_state_seq seq = (*tac)(env(), ios(), ps);
@@ -1648,7 +1648,7 @@ void elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name_set
             return;
         }
 
-        if (auto tac = pre_tactic_to_tactic(subst.instantiate_all(*pre_tac))) {
+        if (auto tac = pre_tactic_to_tactic(*pre_tac)) {
             bool show_failure = true;
             try_using(subst, mvar, ps, *pre_tac, *tac, show_failure);
             return;
diff --git a/src/library/tactic/elaborate.cpp b/src/library/tactic/elaborate.cpp
index e82eb63b63..b5d1cd1133 100644
--- a/src/library/tactic/elaborate.cpp
+++ b/src/library/tactic/elaborate.cpp
@@ -38,7 +38,7 @@ optional<expr> elaborate_with_respect_to(environment const & env, io_state const
     goals const & gs    = s.get_goals();
     if (empty(gs))
         return none_expr();
-    auto ecs = elab(head(gs), ngen.mk_child(), e, report_unassigned);
+    auto ecs   = elab(head(gs), ngen.mk_child(), e, report_unassigned);
     expr new_e = ecs.first;
     buffer<constraint> cs;
     to_buffer(ecs.second, cs);
diff --git a/tests/lean/change_tac_fail.lean b/tests/lean/change_tac_fail.lean
new file mode 100644
index 0000000000..1718ee7e3c
--- /dev/null
+++ b/tests/lean/change_tac_fail.lean
@@ -0,0 +1,12 @@
+import data.list
+open list
+
+variable {T : Type}
+
+theorem append.assoc : ∀ (s t u : list T), s ++ t ++ u = s ++ (t ++ u)
+| append.assoc nil t u      := by esimp
+| append.assoc (a :: l) t u :=
+  begin
+    change a :: (l ++ t ++ u) = (a :: l) ++ (t ++ a),
+    rewrite append.assoc
+  end
diff --git a/tests/lean/change_tac_fail.lean.expected.out b/tests/lean/change_tac_fail.lean.expected.out
new file mode 100644
index 0000000000..4778a96b7a
--- /dev/null
+++ b/tests/lean/change_tac_fail.lean.expected.out
@@ -0,0 +1,8 @@
+change_tac_fail.lean:10:47: error: type mismatch at application
+  t ++ a
+term
+  a
+has type
+  T
+but is expected to have type
+  list T