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..f27ba2444a55188b78eff58c86ba89306983084c 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.
 
@@ -1088,6 +1097,7 @@ Ltac ltac_tactics.string_to_ident_hook ::=
   make_string_to_ident_hook ltac:(fun s => lazymatch s with
                                         | "HP2" => ident:(HP2)
                                         | "H" => ident:(H)
+                                        | "y" => ident:(y)
                                         | _ => fail 100 s
                                         end).
 
@@ -1102,6 +1112,10 @@ Proof.
   exact (Himpl HP2).
 Qed.
 
+Lemma test_iIntros_forall_pure_named (Ψ: nat → PROP) :
+  (∀ x : nat, Ψ x) ⊢ ∀ x : nat, Ψ x.
+Proof. iIntros "HP". iIntros "%y". iApply ("HP" $! y). Qed.
+
 Check "test_not_fresh".
 Lemma test_not_fresh P1 (P2: Prop) (H:P2) :
   P1 ∗ ⌜P2⌝ -∗ P1 ∗ ⌜P2⌝.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index aa53de8907b9a865e48e5f51c4afc5b7811eb013..b03db6a661c56c7bca5097e878b0d778c522d094 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1525,7 +1525,9 @@ Ltac iIntros_go pats startproof :=
     | false => idtac
     end
   (* Optimizations to avoid generating fresh names *)
-  | IPure :: ?pats => iIntro (?); iIntros_go pats startproof
+  | IPure (IGallinaNamed ?s) :: ?pats => let i := string_to_ident s in
+                                         iIntro (i); 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