From bc677d5e161a133f4811a4a76b02565b98976f98 Mon Sep 17 00:00:00 2001
From: Joseph Tassarotti
Date: Wed, 22 May 2019 15:58:01 -0400
Subject: [PATCH] Fix error message in iOrDestruct.
---
tests/proofmode.ref | 8 ++++++++
tests/proofmode.v | 6 ++++++
theories/proofmode/ltac_tactics.v | 23 +++++++++--------------
3 files changed, 23 insertions(+), 14 deletions(-)
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 5f050bee..35af41d6 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -606,6 +606,14 @@ In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"", last call failed.
Tactic failure: iDestruct: (IList [[IClear (sel_patterns.SelIdent "HP")]])
invalid.
+"iOrDestruct_fail"
+ : string
+The command has indeed failed with message:
+Ltac call to "iOrDestruct (constr) as (constr) (constr)" failed.
+Tactic failure: iOrDestruct: "H'" or "H2" not fresh.
+The command has indeed failed with message:
+Ltac call to "iOrDestruct (constr) as (constr) (constr)" failed.
+Tactic failure: iOrDestruct: "H1" or "H'" not fresh.
"iApply_fail"
: string
The command has indeed failed with message:
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 3e568709..07af70c4 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -865,6 +865,12 @@ Check "iDestruct_fail".
Lemma iDestruct_fail P : P -∗ P.
Proof. iIntros "HP". Fail iDestruct "HP" as "{HP}". Fail iDestruct "HP" as "[{HP}]". Abort.
+Check "iOrDestruct_fail".
+Lemma iOrDestruct_fail P : (P ∨ P) -∗ P -∗ P.
+Proof.
+ iIntros "H H'". Fail iOrDestruct "H" as "H'" "H2". Fail iOrDestruct "H" as "H1" "H'".
+Abort.
+
Check "iApply_fail".
Lemma iApply_fail P Q : P -∗ Q.
Proof. iIntros "HP". Fail iApply "HP". Abort.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index cbf51a05..e3e78800 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1095,7 +1095,7 @@ Tactic Notation "iRight" :=
fail "iRight:" P "not a disjunction"
|(* subgoal *)].
-Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
+Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
eapply tac_or_destruct with H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
[pm_reflexivity ||
let H := pretty_ident H in
@@ -1103,19 +1103,14 @@ Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
|iSolveTC ||
let P := match goal with |- IntoOr ?P _ _ => P end in
fail "iOrDestruct: cannot destruct" P
- | pm_reduce; split;
- [ lazymatch goal with
- | |- False =>
- let H1 := pretty_ident H1 in
- fail "iOrDestruct:" H1 "not fresh"
- | _ => idtac (* subgoal 1 *)
- end
- | lazymatch goal with
- | |- False =>
- let H1 := pretty_ident H1 in
- fail "iOrDestruct:" H1 "not fresh"
- | _ => idtac (* subgoal 2 *)
- end ]].
+ | pm_reduce;
+ lazymatch goal with
+ | |- False =>
+ let H1 := pretty_ident H1 in
+ let H2 := pretty_ident H2 in
+ fail "iOrDestruct:" H1 "or" H2 "not fresh"
+ | _ => split
+ end].
(** * Conjunction and separating conjunction *)
Tactic Notation "iSplit" :=
--
GitLab