From 88d1650aa4bb8e55e2c551b8b8fad81d1fb141f9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 4 Aug 2023 16:06:37 +0200
Subject: [PATCH] add a test documenting recently changed behavior

---
 tests/proofmode.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index 31c0c4168..9f54e2d53 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.
-- 
GitLab