Commit bc677d5e authored by Joseph Tassarotti's avatar Joseph Tassarotti

Fix error message in iOrDestruct.

parent be28173f
...@@ -606,6 +606,14 @@ In nested Ltac calls to "iDestruct (open_constr) as (constr)", ...@@ -606,6 +606,14 @@ In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypGo>", last call failed. "<iris.proofmode.ltac_tactics.iDestructHypGo>", last call failed.
Tactic failure: iDestruct: (IList [[IClear (sel_patterns.SelIdent "HP")]]) Tactic failure: iDestruct: (IList [[IClear (sel_patterns.SelIdent "HP")]])
invalid. 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" "iApply_fail"
: string : string
The command has indeed failed with message: The command has indeed failed with message:
......
...@@ -865,6 +865,12 @@ Check "iDestruct_fail". ...@@ -865,6 +865,12 @@ Check "iDestruct_fail".
Lemma iDestruct_fail P : P - <absorb> P. Lemma iDestruct_fail P : P - <absorb> P.
Proof. iIntros "HP". Fail iDestruct "HP" as "{HP}". Fail iDestruct "HP" as "[{HP}]". Abort. 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". Check "iApply_fail".
Lemma iApply_fail P Q : P - Q. Lemma iApply_fail P Q : P - Q.
Proof. iIntros "HP". Fail iApply "HP". Abort. Proof. iIntros "HP". Fail iApply "HP". Abort.
......
...@@ -1095,7 +1095,7 @@ Tactic Notation "iRight" := ...@@ -1095,7 +1095,7 @@ Tactic Notation "iRight" :=
fail "iRight:" P "not a disjunction" fail "iRight:" P "not a disjunction"
|(* subgoal *)]. |(* 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) *) eapply tac_or_destruct with H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
[pm_reflexivity || [pm_reflexivity ||
let H := pretty_ident H in let H := pretty_ident H in
...@@ -1103,19 +1103,14 @@ Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) := ...@@ -1103,19 +1103,14 @@ Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
|iSolveTC || |iSolveTC ||
let P := match goal with |- IntoOr ?P _ _ => P end in let P := match goal with |- IntoOr ?P _ _ => P end in
fail "iOrDestruct: cannot destruct" P fail "iOrDestruct: cannot destruct" P
| pm_reduce; split; | pm_reduce;
[ lazymatch goal with lazymatch goal with
| |- False => | |- False =>
let H1 := pretty_ident H1 in let H1 := pretty_ident H1 in
fail "iOrDestruct:" H1 "not fresh" let H2 := pretty_ident H2 in
| _ => idtac (* subgoal 1 *) fail "iOrDestruct:" H1 "or" H2 "not fresh"
end | _ => split
| lazymatch goal with end].
| |- False =>
let H1 := pretty_ident H1 in
fail "iOrDestruct:" H1 "not fresh"
| _ => idtac (* subgoal 2 *)
end ]].
(** * Conjunction and separating conjunction *) (** * Conjunction and separating conjunction *)
Tactic Notation "iSplit" := Tactic Notation "iSplit" :=
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment