diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 63edca3efe3deb94a723d554ec6746c367c71763..1434459a97d97cb04f8c826ca475a8882ec9b47e 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1589,7 +1589,7 @@ Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
 
 Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1) ")"
     constr(pat) :=
-  iExistDestruct H as x1 H; iDestructHyp H as @ pat.
+  iExistDestruct H as x1 H; iDestructHyp H as pat.
 Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) ")" constr(pat) :=
   iExistDestruct H as x1 H; iDestructHyp H as ( x2 ) pat.