From e6abed1df11cebf2b569d8c4d290f3ec18f01869 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 4 Aug 2023 08:38:44 +0200
Subject: [PATCH] =?UTF-8?q?Fix=20bug=20in=20iL=C3=B6b=20caused=20by=20n-ar?=
 =?UTF-8?q?y=20intros=20change.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 iris/proofmode/ltac_tactics.v |  2 +-
 tests/proofmode.v             | 11 +++++++++++
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 3d3ab1058..33e03541c 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 e78302a57..d9d4ff403 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.
-- 
GitLab