diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 5cb16a875a70da6928a5aa79c89412ce073f498f..47127e687024fd9ad9da4d2e00340d944ac6c1c7 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1419,7 +1419,9 @@ Local Ltac string_to_ident s :=
   end.
 
 (** * Basic destruct tactic *)
-Local Ltac iDestructHypGo Hz pat :=
+
+(** [pat0] is the unparsed pattern, and is only used in error messages *)
+Local Ltac iDestructHypGo Hz pat0 pat :=
   lazymatch pat with
   | IFresh =>
      lazymatch Hz with
@@ -1430,20 +1432,38 @@ Local Ltac iDestructHypGo Hz pat :=
   | IFrame => iFrameHyp Hz
   | IIdent ?y => iRename Hz into y
   | IList [[]] => iExFalso; iExact Hz
-  | IList [[?pat1; IDrop]] => iAndDestructChoice Hz as Left Hz; iDestructHypGo Hz pat1
-  | IList [[IDrop; ?pat2]] => iAndDestructChoice Hz as Right Hz; iDestructHypGo Hz 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 pat1; iDestructHypGo Hy pat2
-  | IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [iDestructHypGo Hz pat1|iDestructHypGo Hz 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
   | IRewrite Right => iPure Hz as ->
   | IRewrite Left => iPure Hz as <-
-  | IIntuitionistic ?pat => iIntuitionistic Hz; iDestructHypGo Hz pat
-  | ISpatial ?pat => iSpatial Hz; iDestructHypGo Hz pat
-  | IModalElim ?pat => iModCore Hz; iDestructHypGo Hz pat
-  | _ => fail "iDestruct:" pat "invalid"
+  | 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 "is not supported due to" pat
   end.
 Local Ltac iDestructHypFindPat Hgo pat found pats :=
   lazymatch pats with
@@ -1457,7 +1477,7 @@ Local Ltac iDestructHypFindPat Hgo pat found pats :=
   | IClearFrame ?H :: ?pats => iFrame H; iDestructHypFindPat Hgo pat found pats
   | ?pat1 :: ?pats =>
      lazymatch found with
-     | false => iDestructHypGo Hgo pat1; iDestructHypFindPat Hgo pat true pats
+     | false => iDestructHypGo Hgo pat pat1; iDestructHypFindPat Hgo pat true pats
      | true => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
      end
   end.
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index a3799261570cbfd04c93fbaca4faa22e8d71c62a..bbaf4e29726e4e07331b9210bbc3d9716e7f065a 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -631,14 +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: (IList [[IClear (sel_patterns.SelIdent "HP")]])
-invalid.
+Tactic failure: iDestruct: "// H" is not supported due to IDone.
 The command has indeed failed with message:
-Tactic failure: iDestruct: "HP HQ HR"
+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]" 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 a7c3a1dc43aa303eef66c3aef6fccca945a075b1..331ea7d5b781d72b6591e316c4837ece76657b7b 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1226,9 +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}]".
-  Fail iDestruct "HP" as "HP HQ HR".
+  (* 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]".
+  Fail iDestruct "HP" as "[HP HQ|HR]".
 Abort.
 
 Check "iOrDestruct_fail".