From ce3387b246c15b2ef8decf4e3f3880a39e9c25e2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 20 Jun 2017 12:04:07 -0700
Subject: [PATCH] fix(library/tactic/change_tactic): fixes #1686

---
 src/library/tactic/change_tactic.cpp |  7 ++++---
 tests/lean/run/1686.lean             | 26 ++++++++++++++++++++++++++
 2 files changed, 30 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/1686.lean

diff --git a/src/library/tactic/change_tactic.cpp b/src/library/tactic/change_tactic.cpp
index a1027fb156..8822234bd5 100644
--- a/src/library/tactic/change_tactic.cpp
+++ b/src/library/tactic/change_tactic.cpp
@@ -19,7 +19,8 @@ vm_obj change_core(expr const & e, bool check, tactic_state const & s) {
         type_context ctx         = mk_type_context_for(s);
         if (!check || ctx.is_def_eq(e, g->get_type())) {
             auto mctx    = ctx.mctx();
-            expr new_M   = mctx.mk_metavar_decl(g->get_context(), e);
+            expr new_e   = mctx.instantiate_mvars(e);
+            expr new_M   = mctx.mk_metavar_decl(g->get_context(), new_e);
             /*
                We use the proof term
 
@@ -41,8 +42,8 @@ vm_obj change_core(expr const & e, bool check, tactic_state const & s) {
             };
             return tactic::mk_exception(thunk, s);
         }
-    } catch (exception & e) {
-        return tactic::mk_exception(e, s);
+    } catch (exception & ex) {
+        return tactic::mk_exception(ex, s);
     }
 }
 
diff --git a/tests/lean/run/1686.lean b/tests/lean/run/1686.lean
new file mode 100644
index 0000000000..3f83c58aec
--- /dev/null
+++ b/tests/lean/run/1686.lean
@@ -0,0 +1,26 @@
+def f (n : ℕ) := n + n
+def g (n : ℕ) := 2*n
+
+example (n : ℕ) : g (n+1) = f n + 2 :=
+begin
+ change 2 * (n + 1) = f n + 2,
+ unfold f,
+ guard_target 2 * (n + 1) = n + n + 2,
+ admit
+end
+
+example (n : ℕ) : g (n+1) = f n + 2 :=
+begin
+ change g (n + 1) with 2 * (n+1),
+ unfold f,
+ guard_target 2 * (n + 1) = n + n + 2,
+ admit
+end
+
+example (n : ℕ) : g (n+1) = f n + 2 :=
+begin
+ change 2 * (n + 1) = _,
+ unfold f,
+ guard_target 2 * (n + 1) = n + n + 2,
+ admit
+end