From 650261fcf167ec5b4b0238c5a17e726f2c419f78 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 13 Nov 2017 20:27:45 +0100
Subject: [PATCH] Remove spurious `iStartProof`.
---
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 ca5444076..6764fa796 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1263,7 +1263,7 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
| 1 => repeat iIntroForall; let H := iFresh in iIntro H; tac H
| S ?n' => repeat iIntroForall; let H := iFresh in iIntro H; go n'
end in
- intros; iStartProof; go n in
+ intros; go n in
lazymatch type of lem with
| nat => intro_destruct lem
| Z => (* to make it work in Z_scope. We should just be able to bind
--
GitLab