diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 035cf8fb18e9d517cd1d6ba207e4d53cecd9864d..7f3d22d44be683dea4e1cc8be87017ca4d8ce258 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -570,7 +570,7 @@ Local Tactic Notation "iIntroForall" :=
   lazymatch goal with
   | |- ∀ _, ?P => fail
   | |- ∀ _, _ => intro
-  | |- _ ⊢ (∀ _, _) => iIntro {?}
+  | |- _ ⊢ (∀ x : _, _) => iIntro {x}
   end.
 Local Tactic Notation "iIntro" :=
   lazymatch goal with