diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 675436b3a3cf0c3602f6a71dd4e55c2f67381960..aec6cbf8dbe22b79aa5996986c0975c60f417e6c 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -672,8 +672,26 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
     | IAlwaysElim ?pat => iPersistent Hz; go Hz pat
     | IModalElim ?pat => iModCore Hz; go Hz pat
     | _ => fail "iDestruct:" pat "invalid"
-    end
-  in let pat := intro_pat.parse_one pat in go H pat.
+    end in
+  let rec find_pat found pats :=
+    lazymatch pats with
+    | [] =>
+      match found with
+      | true => idtac
+      | false => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
+      end
+    | ISimpl :: ?pats => simpl; find_pat found pats
+    | IClear ?H :: ?pats => iClear H; find_pat found pats
+    | IClearFrame ?H :: ?pats => iFrame H; find_pat found pats
+    | ?pat :: ?pats =>
+       match found with
+       | false => go H pat; find_pat true pats
+       | true => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
+       end
+    | _ => fail "hallo" pats
+    end in
+  let pats := intro_pat.parse pat in
+  find_pat false pats.
 
 Local Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1) ")"
     constr(pat) :=