From 3b96108310b6ac0f785a1d550247a5bfd4ef2e11 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 15 Dec 2018 11:30:24 +0100
Subject: [PATCH] Simplify implementation of `iRevertIntros`.
---
theories/proofmode/ltac_tactics.v | 7 ++++---
1 file changed, 4 insertions(+), 3 deletions(-)
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index bccbbcf85..8efdfd4af 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1464,9 +1464,10 @@ Tactic Notation "iRevertIntros" constr(Hs) "with" tactic(tac) :=
| ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
| ESelIdent ?p ?H :: ?Hs =>
iRevert H; go Hs;
- let H' :=
- match p with true => constr:([IAlwaysElim (IIdent H)]) | false => H end in
- iIntros H'
+ match p with
+ | true => iIntro #H
+ | false => iIntro H
+ end
end in
try iStartProof; let Hs := iElaborateSelPat Hs in go Hs.
--
GitLab