diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 6da1b9bb36336f82ed0a138ffcb06a2af585f2ad..3d3c2b9b1d2095cafdbe982a50931ef81e0f1e4f 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -755,7 +755,7 @@ Local Tactic Notation "iIntroForall" :=
   lazymatch goal with
   | |- ∀ _, ?P => fail
   | |- ∀ _, _ => intro
-  | |- _ ⊢ (∀ x : _, _) => iIntro (x)
+  | |- _ ⊢ (∀ x : _, _) => let x' := fresh x in iIntro (x')
   end.
 Local Tactic Notation "iIntro" :=
   try iStartProof;