Let iIntros "*" reuse names of binders.

We may want to do the same for iIntros ? and iDestruct "H" as {?} "H",
but that requires more work. However, I do not think I want to rely on
names chosen this way.

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