diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 2d7a50bc77276f9f670aff5eaca8695b8b66b259..e5444b291c255460e09ac81682b2035bfaceb347 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -830,7 +830,6 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
        | 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.