diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 3b5776176f25a7c8d051a5c8b27588944ac51776..b22f2edf5bdfcdf81aa9a7362a9e218f9d555c5c 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -77,6 +77,17 @@
   --------------------------------------∗
   Q
   
+"test_iIntros_forall_pure"
+     : string
+1 subgoal
+  
+  PROP : sbi
+  Ψ : nat → PROP
+  a : nat
+  ============================
+  --------------------------------------∗
+  Ψ a → Ψ a
+  
 The command has indeed failed with message:
 No applicable tactic.
 The command has indeed failed with message:
diff --git a/tests/proofmode.v b/tests/proofmode.v
index f4fefc0a57d41df816a19004e8b407f0ce9504ab..01e0189a5d1f77949c43c340dcc4e16a5e552c32 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -119,6 +119,15 @@ Proof. iIntros "-#HQ". done. Qed.
 Lemma test_iIntros_pure (ψ φ : Prop) P : ψ → ⊢ ⌜ φ ⌝ → P → ⌜ φ ∧ ψ ⌝ ∧ P.
 Proof. iIntros (??) "H". auto. Qed.
 
+Check "test_iIntros_forall_pure".
+Lemma test_iIntros_forall_pure (Ψ: nat → PROP) :
+  ⊢ ∀ x : nat, Ψ x → Ψ x.
+Proof.
+  iIntros "%".
+  (* should be a trivial implication now *)
+  Show. auto.
+Qed.
+
 Lemma test_iIntros_pure_not : ⊢@{PROP} ⌜ ¬False ⌝.
 Proof. by iIntros (?). Qed.
 
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index aa53de8907b9a865e48e5f51c4afc5b7811eb013..34b7029bfcc33404e602314ca3bf4e7ca734c390 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1525,7 +1525,7 @@ Ltac iIntros_go pats startproof :=
     | false => idtac
     end
   (* Optimizations to avoid generating fresh names *)
-  | IPure :: ?pats => iIntro (?); iIntros_go pats startproof
+  | IPure IGallinaAnon :: ?pats => iIntro (?); iIntros_go pats startproof
   | IIntuitionistic (IIdent ?H) :: ?pats => iIntro #H; iIntros_go pats false
   | IDrop :: ?pats => iIntro _; iIntros_go pats startproof
   | IIdent ?H :: ?pats => iIntro H; iIntros_go pats startproof