From 4c38ac070dcb86d67ddbb9a57a831c1b64bc01e3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 4 Jan 2017 18:19:44 +0100
Subject: [PATCH] Let iRevertIntros ensure that we are in the proofmode.
This fixes issue #61.
---
theories/proofmode/tactics.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index d5c577970..02c4e2281 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -861,7 +861,7 @@ Tactic Notation "iRevertIntros" constr(Hs) "with" tactic(tac) :=
match p with true => constr:([IAlwaysElim (IName H)]) | false => H end in
iIntros H'
end in
- iElaborateSelPat Hs go.
+ try iStartProof; iElaborateSelPat Hs go.
Tactic Notation "iRevertIntros" "(" ident(x1) ")" constr(Hs) "with" tactic(tac):=
iRevertIntros Hs with (iRevert (x1); tac; iIntros (x1)).
--
GitLab