add a test documenting recently changed behavior

tests/proofmode.v

@@ -1485,6 +1485,17 @@ Proof. auto. Qed.
 
 Lemma test_auto_wand_iff P : ⊢ P ∗-∗ P.
 Proof. auto. Qed.
+
+Lemma test_iIntros_auto_name_used_later (Φ: nat → PROP) :
+  ⊢ ∀ x y, Φ (x+y).
+Proof.
+  (* This test documents a difference between [intros ...] and [iIntros (...)]:
+  the latter will pick [x] as the name for the [?] here (matching the name in the goal)
+  and then fail later when another [x] is attempted to be introduced. [intros] will
+  somehow realize that [x] is coming later, and pick a different name for the [?]. *)
+  Fail iIntros (? x).
+Abort.
+
 End tests.
 
 Section parsing_tests.