From c3d4c468e6f3eda01acf0cf85f1a40d147ebe5fc Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 4 Jul 2017 11:04:20 +0200
Subject: [PATCH] fix(init/meta/interactive): whnf in `assume` tactic

---
 library/init/meta/interactive.lean           | 1 +
 library/init/meta/smt/interactive.lean       | 9 +--------
 tests/lean/keyword_tactics.lean              | 6 ++++++
 tests/lean/keyword_tactics.lean.expected.out | 2 +-
 4 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 81ce3f7fa3..367b03b9c1 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -523,6 +523,7 @@ meta def «assume» (p : parse parse_binders) : tactic unit :=
 list.mfor' p $ λ b,
   do t ← target,
      when (not $ t.is_pi ∨ t.is_let) whnf_target,
+     t ← target,
      when (not $ t.is_pi ∨ t.is_let) $
        fail "assume tactic failed, Pi/let expression expected",
      ty ← i_to_expr b.local_type,
diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean
index 1e543c643d..e8721e1e83 100644
--- a/library/init/meta/smt/interactive.lean
+++ b/library/init/meta/smt/interactive.lean
@@ -78,14 +78,7 @@ meta def exact (q : parse texpr) : smt_tactic unit :=
 tactic.interactive.exact q
 
 meta def «assume» (p : parse parse_binders) : smt_tactic unit :=
-list.mfor' p $ λ b,
-  do t ← tactic.target,
-     when (not $ t.is_pi ∨ t.is_let) tactic.whnf_target,
-     when (not $ t.is_pi ∨ t.is_let) $
-       fail "assume tactic failed, Pi/let expression expected",
-     ty ← tactic.i_to_expr b.local_type,
-     tactic.unify ty t.binding_domain,
-     smt_tactic.intro_lst [b.local_pp_name]
+tactic.interactive.assume p
 
 meta def «suppose» (h : parse ident?) (q : parse (tk ":" *> texpr)?) : smt_tactic unit :=
 let h := h.get_or_else `this in
diff --git a/tests/lean/keyword_tactics.lean b/tests/lean/keyword_tactics.lean
index 40f65485c3..0d667f39d1 100644
--- a/tests/lean/keyword_tactics.lean
+++ b/tests/lean/keyword_tactics.lean
@@ -10,6 +10,12 @@ begin
   apply n
 end
 
+example : ¬false :=
+begin
+  assume contr,
+  apply contr
+end
+
 example : ℕ → ℕ → ℕ :=
 begin
   assume n m : bool,
diff --git a/tests/lean/keyword_tactics.lean.expected.out b/tests/lean/keyword_tactics.lean.expected.out
index 0acb8e6c36..96a624269d 100644
--- a/tests/lean/keyword_tactics.lean.expected.out
+++ b/tests/lean/keyword_tactics.lean.expected.out
@@ -1,4 +1,4 @@
-keyword_tactics.lean:15:2: error: unify tactic failed, failed to unify
+keyword_tactics.lean:21:2: error: unify tactic failed, failed to unify
   bool : Type
 and
   ℕ : Type