From c476d1099c792d500e6df60f2560a6d9ebeb063e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 26 Oct 2016 22:06:33 +0200
Subject: [PATCH] Improve error message of iIntros.

This fixes issue 39.
---
 proofmode/tactics.v | 21 ++++++++++-----------
 1 file changed, 10 insertions(+), 11 deletions(-)

diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 23848b1b8..d4d5431ad 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -678,17 +678,16 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1)
   iExistDestruct H as x1 H; iDestructHyp H as ( x2 x3 x4 x5 x6 x7 x8 ) pat.
 
 (** * Introduction tactic *)
-Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" := first
-  [ (* (∀ _, _) *) apply tac_forall_intro; intros x
-  | (* (?P → _) *) eapply tac_impl_intro_pure;
-     [let P := match goal with |- IntoPure ?P _ => P end in
-      apply _ || fail "iIntro:" P "not pure"
-     |intros x]
-  | (* (?P -★ _) *) eapply tac_wand_intro_pure;
-     [let P := match goal with |- IntoPure ?P _ => P end in
-      apply _ || fail "iIntro:" P "not pure"
-     |intros x]
-  |intros x].
+Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
+  try first
+    [(* (∀ _, _) *) apply tac_forall_intro
+    |(* (?P → _) *) eapply tac_impl_intro_pure;
+      [let P := match goal with |- IntoPure ?P _ => P end in
+       apply _ || fail "iIntro:" P "not pure"|]
+    |(* (?P -★ _) *) eapply tac_wand_intro_pure;
+      [let P := match goal with |- IntoPure ?P _ => P end in
+       apply _ || fail "iIntro:" P "not pure"|]];
+  intros x.
 
 Local Tactic Notation "iIntro" constr(H) := first
   [ (* (?Q → _) *)
-- 
GitLab