diff --git a/tests/proofmode.v b/tests/proofmode.v
index 01e0189a5d1f77949c43c340dcc4e16a5e552c32..f27ba2444a55188b78eff58c86ba89306983084c 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1097,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).
 
@@ -1111,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 34b7029bfcc33404e602314ca3bf4e7ca734c390..b03db6a661c56c7bca5097e878b0d778c522d094 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1525,6 +1525,8 @@ Ltac iIntros_go pats startproof :=
     | false => idtac
     end
   (* Optimizations to avoid generating fresh names *)
+  | 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