diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 572cd8a09d17cd4cc04269d3091feba7459cb07e..bbaf4e29726e4e07331b9210bbc3d9716e7f065a 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -631,15 +631,20 @@ Tactic failure: iElaborateSelPat: "H" not found.
 "iDestruct_fail"
      : string
 The command has indeed failed with message:
-Tactic failure: iDestruct: "{HP}"
-should contain exactly one proper introduction pattern.
+Tactic failure: iDestruct: "[{HP}]" has just a single conjunct.
+The command has indeed failed with message:
+Tactic failure: iDestruct: "// H" is not supported due to IDone.
 The command has indeed failed with message:
-Tactic failure: iDestruct: "[{HP}]" invalid.
+Tactic failure: iDestruct: "HP //"
+should contain exactly one proper introduction pattern.
 The command has indeed failed with message:
 Tactic failure: iDestruct: "[HP HQ HR]" has too many conjuncts.
 The command has indeed failed with message:
-Tactic failure: iDestruct: "HP HQ HR"
-should contain exactly one proper introduction pattern.
+Tactic failure: iDestruct: "[HP|HQ|HR]" has too many disjuncts.
+The command has indeed failed with message:
+Tactic failure: iDestruct: "[HP]" has just a single conjunct.
+The command has indeed failed with message:
+Tactic failure: iDestruct: in "[HP HQ|HR]" a disjunct has multiple patterns.
 "iOrDestruct_fail"
      : string
 The command has indeed failed with message:
diff --git a/tests/proofmode.v b/tests/proofmode.v
index c6d24d1a98d829e3dbc6f5593eb559c8273df1b1..331ea7d5b781d72b6591e316c4837ece76657b7b 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1226,10 +1226,18 @@ Check "iDestruct_fail".
 Lemma iDestruct_fail P : P -∗ <absorb> P.
 Proof.
   iIntros "HP".
-  Fail iDestruct "HP" as "{HP}".
   Fail iDestruct "HP" as "[{HP}]".
+  (* IDone is unsupported (see issue #380) *)
+  Fail iDestruct "HP" as "// H".
+  (* fails due to not having "one proper intro pattern" (see issue #380) *)
+  Fail iDestruct "HP" as "HP //".
+  (* both of these work *)
+  iDestruct "HP" as "HP /=".
+  iDestruct "HP" as "/= HP".
   Fail iDestruct "HP" as "[HP HQ HR]".
-  Fail iDestruct "HP" as "HP HQ HR".
+  Fail iDestruct "HP" as "[HP|HQ|HR]".
+  Fail iDestruct "HP" as "[HP]".
+  Fail iDestruct "HP" as "[HP HQ|HR]".
 Abort.
 
 Check "iOrDestruct_fail".
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index c83c7dddf815b79b11577f8551dc56c0aaf3aa30..0e5b695d062c5e7a6dceb29e1686993c5e513b3a 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1419,7 +1419,8 @@ Local Ltac string_to_ident s :=
   end.
 
 (** * Basic destruct tactic *)
-(* pat0 is the unparsed pattern and is only used in error messages *)
+
+(** [pat0] is the unparsed pattern, and is only used in error messages *)
 Local Ltac iDestructHypGo Hz pat0 pat :=
   lazymatch pat with
   | IFresh =>
@@ -1431,12 +1432,29 @@ Local Ltac iDestructHypGo Hz pat0 pat :=
   | IFrame => iFrameHyp Hz
   | IIdent ?y => iRename Hz into y
   | IList [[]] => iExFalso; iExact Hz
-  | IList [[?pat1; IDrop]] => iAndDestructChoice Hz as Left Hz; iDestructHypGo Hz pat0 pat1
-  | IList [[IDrop; ?pat2]] => iAndDestructChoice Hz as Right Hz; iDestructHypGo Hz pat0 pat2
+
+  (* conjunctive patterns like [H1 H2] *)
+  | IList [[?pat1; IDrop]] =>
+     iAndDestructChoice Hz as Left Hz;
+     iDestructHypGo Hz pat0 pat1
+  | IList [[IDrop; ?pat2]] =>
+     iAndDestructChoice Hz as Right Hz;
+     iDestructHypGo Hz pat0 pat2
   | IList [[?pat1; ?pat2]] =>
-     let Hy := iFresh in iAndDestruct Hz as Hz Hy; iDestructHypGo Hz pat0 pat1; iDestructHypGo Hy pat0 pat2
-  | IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [iDestructHypGo Hz pat0 pat1|iDestructHypGo Hz pat0 pat2]
+     let Hy := iFresh in iAndDestruct Hz as Hz Hy;
+     iDestructHypGo Hz pat0 pat1; iDestructHypGo Hy pat0 pat2
   | IList [_ :: _ :: _] => fail "iDestruct:" pat0 "has too many conjuncts"
+  | IList [[_]] => fail "iDestruct:" pat0 "has just a single conjunct"
+
+  (* disjunctive patterns like [H1|H2] *)
+  | IList [[?pat1];[?pat2]] =>
+     iOrDestruct Hz as Hz Hz;
+     [iDestructHypGo Hz pat0 pat1|iDestructHypGo Hz pat0 pat2]
+  (* this matches a list of three or more disjunctions [H1|H2|H3] *)
+  | IList (_ :: _ :: _ :: _) => fail "iDestruct:" pat0 "has too many disjuncts"
+  (* the above patterns don't match [H1 H2|H3] *)
+  | IList [_;_] => fail "iDestruct: in" pat0 "a disjunct has multiple patterns"
+
   | IPure IGallinaAnon => iPure Hz as ?
   | IPure (IGallinaNamed ?s) => let x := string_to_ident s in
                                 iPure Hz as x
@@ -1445,7 +1463,7 @@ Local Ltac iDestructHypGo Hz pat0 pat :=
   | IIntuitionistic ?pat => iIntuitionistic Hz; iDestructHypGo Hz pat0 pat
   | ISpatial ?pat => iSpatial Hz; iDestructHypGo Hz pat0 pat
   | IModalElim ?pat => iModCore Hz; iDestructHypGo Hz pat0 pat
-  | _ => fail "iDestruct:" pat0 "invalid"
+  | _ => fail "iDestruct:" pat0 "is not supported due to" pat
   end.
 Local Ltac iDestructHypFindPat Hgo pat found pats :=
   lazymatch pats with