From bf73b3b91a536c5df5cc6d578bb3f304220e17b6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 14 Nov 2017 11:35:51 +0100
Subject: [PATCH] Make iDestruct/iMod/... perform an `iStartProof` to get
better error messages.
---
theories/proofmode/tactics.v | 1 +
1 file changed, 1 insertion(+)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 6764fa796..94c2de629 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1274,6 +1274,7 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
Also, rule out cases in which it does not make sense to copy, namely when
destructing a lemma (instead of a hypothesis) or a spatial hyopthesis
(which cannot be kept). *)
+ iStartProof;
lazymatch ident with
| None => iPoseProofCore lem as p false tac
| Some ?H =>
--
GitLab