From ae63e7a1c1df33ca1d6017efd9d5929256b84e71 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 1 Sep 2017 15:49:21 +0200
Subject: [PATCH] Fix error message of iDestruct.
---
theories/proofmode/tactics.v | 8 ++++++--
1 file changed, 6 insertions(+), 2 deletions(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index e28c9ac2a..4329266a7 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -774,8 +774,12 @@ Tactic Notation "iSplitR" := iSplitL "".
Local Tactic Notation "iAndDestruct" constr(H) "as" constr(H1) constr(H2) :=
eapply tac_and_destruct with _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
[env_reflexivity || fail "iAndDestruct:" H "not found"
- |apply _ ||
- let P := match goal with |- IntoSep _ ?P _ _ => P end in
+ |env_cbv; apply _ ||
+ let P :=
+ lazymatch goal with
+ | |- IntoSep ?P _ _ => P
+ | |- IntoAnd _ ?P _ _ => P
+ end in
fail "iAndDestruct: cannot destruct" P
|env_reflexivity || fail "iAndDestruct:" H1 "or" H2 " not fresh"|].
--
GitLab