From fb2186334a5523bf8048b8d96dcdb710c1b46e98 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 21 Aug 2017 14:51:30 -0700
Subject: [PATCH] 
 fix(library/init/meta/relation_tactics,library/tactic/subst_tactic): fixes
 #1772

---
 library/init/meta/relation_tactics.lean | 2 +-
 src/library/tactic/subst_tactic.cpp     | 9 +++++----
 tests/lean/run/1772.lean                | 8 ++++++++
 3 files changed, 14 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/run/1772.lean

diff --git a/library/init/meta/relation_tactics.lean b/library/init/meta/relation_tactics.lean
index 8224b7c08a..1a77e1d2db 100644
--- a/library/init/meta/relation_tactics.lean
+++ b/library/init/meta/relation_tactics.lean
@@ -10,7 +10,7 @@ namespace tactic
 open expr
 
 private meta def relation_tactic (md : transparency) (op_for : environment → name → option name) (tac_name : string) : tactic unit :=
-do tgt   ← target,
+do tgt   ← target >>= instantiate_mvars,
    env   ← get_env,
    let r := get_app_fn tgt,
    match (op_for env (const_name r)) with
diff --git a/src/library/tactic/subst_tactic.cpp b/src/library/tactic/subst_tactic.cpp
index b27d302c3f..e81bc0c772 100644
--- a/src/library/tactic/subst_tactic.cpp
+++ b/src/library/tactic/subst_tactic.cpp
@@ -40,7 +40,7 @@ expr subst(environment const & env, options const & opts, transparency_mode cons
     lean_assert(mctx.find_metavar_decl(mvar));
     metavar_decl g      = mctx.get_metavar_decl(mvar);
     type_context ctx    = mk_type_context_for(env, opts, mctx, g.get_context(), m);
-    expr H_type         = ctx.infer(H);
+    expr H_type         = ctx.instantiate_mvars(ctx.infer(H));
     expr lhs, rhs;
     lean_verify(is_eq(H_type, lhs, rhs));
     if (symm) std::swap(lhs, rhs);
@@ -129,7 +129,7 @@ vm_obj tactic_subst(expr const & l, tactic_state const & s) {
     optional<local_decl> d     = lctx.find_local_decl(l);
     if (!d)
         return tactic::mk_exception(sstream() << "subst tactic failed, unknown '" << mlocal_pp_name(l) << "' hypothesis", s);
-    expr const & type = d->get_type();
+    expr type = mctx.instantiate_mvars(d->get_type());
     expr lhs, rhs;
     if (is_eq(type, lhs, rhs)) {
         if (is_local(rhs) && !depends_on(lhs, mctx, lctx, rhs)) {
@@ -138,7 +138,7 @@ vm_obj tactic_subst(expr const & l, tactic_state const & s) {
             return tactic_subst_core(d->get_name(), false, s);
         } else {
             return tactic::mk_exception(sstream() << "subst tactic failed, hypothesis '"
-                                       << mlocal_pp_name(l) << "' is not of the form (x = t) or (t = x)", s);
+                                        << mlocal_pp_name(l) << "' is not of the form (x = t) or (t = x)", s);
         }
     } else {
         bool found = false;
@@ -146,7 +146,8 @@ vm_obj tactic_subst(expr const & l, tactic_state const & s) {
         lctx.for_each_after(*d, [&](local_decl const & d2) {
                 if (found) return;
                 expr lhs, rhs;
-                if (is_eq(d2.get_type(), lhs, rhs)) {
+                expr type = mctx.instantiate_mvars(d2.get_type());
+                if (is_eq(type, lhs, rhs)) {
                     if (is_local(lhs) && mlocal_name(lhs) == d->get_name() && !depends_on(rhs, mctx, lctx, lhs)) {
                         found = true;
                         r     = tactic_subst_core(d2.get_name(), false, s);
diff --git a/tests/lean/run/1772.lean b/tests/lean/run/1772.lean
new file mode 100644
index 0000000000..26bdb99efc
--- /dev/null
+++ b/tests/lean/run/1772.lean
@@ -0,0 +1,8 @@
+example (p : Prop) (f : ∀ q : Prop, q → q) : p = p :=
+by apply f _ _; refl
+
+example (p : Prop) (f : ∀ q : Prop, q → q) : p = p :=
+by apply f _ _; transitivity; refl
+
+example (p r : Prop) (f : ∀ q : Prop, (r = q → q) → q) (h2 : r): p :=
+by apply f _ (λ h, _); subst h; assumption