diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 3d3ab10589cc6c00410bfcc18a43d58f9c5d3d47..33e03541cea1a8d329ea23bcb41d102f4ca7bde7 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1839,7 +1839,7 @@ Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ne_ident_list(xs) ")" :=
 Tactic Notation "iLöb" "as" constr (IH) "forall" constr(Hs) :=
   _iLöb0 Hs IH.
 Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ne_ident_list(xs) ")" constr(Hs) :=
-  _iLöb0 xs Hs IH.
+  _iLöb xs Hs IH.
 
 (** * Assert *)
 (* The argument [p] denotes whether [Q] is persistent. It can either be a
diff --git a/tests/proofmode.v b/tests/proofmode.v
index e78302a57fd3e9d545b2577f58cfdc782d188165..d9d4ff403c8676e7498b394dee226c9b0c2ab8ab 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -875,6 +875,17 @@ Proof.
   by iExists (S n).
 Qed.
 
+Lemma test_iLöb_forall `{!BiLöb PROP} P (n : nat) : P ⊢ ⌜ n = n ⌝.
+Proof.
+  iIntros "HP". iLöb as "IH" forall (n) "HP".
+Restart.
+  iIntros "HP". iLöb as "IH" forall "HP".
+Restart.
+  iIntros "HP". iLöb as "IH" forall (n).
+Restart.
+  iIntros "HP". iLöb as "IH".
+Abort.
+
 Lemma test_iInduction_wf (x : nat) P Q :
   □ P -∗ Q -∗ ⌜ (x + 0 = x)%nat ⌝.
 Proof.