diff --git a/tests/proofmode.v b/tests/proofmode.v
index 31c0c4168b4909f54d37b0a936f0141bbfaa54e8..9f54e2d537de0c85a0c6ba197b21d335e8967e37 100644
--- a/tests/proofmode.v
+++ b/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.