From b0ae1102f6aa4cac5b4bce397ad8fa0f5885eaf1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 26 Sep 2017 22:27:01 +0200
Subject: [PATCH] Fix issue #97.
---
theories/proofmode/tactics.v | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index d25a56c5c..4c7069ccb 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -605,6 +605,7 @@ Local Tactic Notation "iForallRevert" ident(x) :=
lazymatch P with
| context [x] => fail 2 "iRevert:" x "is used in hypothesis" H
end) in
+ iStartProof;
let A := type of x in
lazymatch type of A with
| Prop => revert x; first [apply tac_pure_revert|err x]
@@ -623,7 +624,7 @@ Tactic Notation "iRevert" constr(Hs) :=
[env_reflexivity || fail "iRevert:" H "not found"
|env_cbv; go Hs]
end in
- let Hs := iElaborateSelPat Hs in go Hs.
+ let Hs := iElaborateSelPat Hs in iStartProof; go Hs.
Tactic Notation "iRevert" "(" ident(x1) ")" :=
iForallRevert x1.
@@ -938,7 +939,7 @@ Tactic Notation "iIntros" constr(pat) :=
| ?pat :: ?pats =>
let H := iFresh in iIntro H; iDestructHyp H as pat; go pats
end
- in let pats := intro_pat.parse pat in go pats.
+ in let pats := intro_pat.parse pat in iStartProof; go pats.
Tactic Notation "iIntros" := iIntros [IAll].
Tactic Notation "iIntros" "(" simple_intropattern(x1) ")" :=
--
GitLab