diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 5f050bee0a3d8f6e5d00ddaf63c2ca75ddf1537b..35af41d6d799c6bc48723e54a8397a59e40d668a 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 3e56870934f3c92632f0814f31d51fa46a2ca3f8..07af70c40f1bc7f1d439e3d07f9c7986a5822042 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 cbf51a05b593c9e026d99ad3267c571c51583aa4..e3e78800a09f5b42cb10c65d53824d1cff33f65c 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" :=