3 files changed, 24 insertions, 0 deletions
diff --git a/test-suite/output/names.out b/test-suite/output/names.out
new file mode 100644
index 0000000000..90ad4ba090
--- /dev/null
+++ b/test-suite/output/names.out
@@ -0,0 +1,5 @@
+The command has indeed failed with message:
+=> Error: In environment
+   y : nat
+   The term "a y" has type "{y0 : nat | y = y0}"
+    while it is expected to have type "{x : nat | x = y}".
diff --git a/test-suite/output/names.v b/test-suite/output/names.v
new file mode 100644
index 0000000000..b3b5071a03
--- /dev/null
+++ b/test-suite/output/names.v
@@ -0,0 +1,5 @@
+(* Test no clash names occur *)
+(* see bug #2723 *)
+
+Parameter a : forall x, {y:nat|x=y}.
+Fail Definition b y : {x:nat|x=y} := a y.
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index e3183ef279..8e829e061d 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -415,3 +415,17 @@ apply mapfuncomp.
 Abort.
 
 End A.
+
+(* Check "with" clauses refer to names as they are printed *)
+
+Definition hide p := forall n:nat, p = n.
+
+Goal forall n, (forall n, n=0) -> hide n -> n=0.
+unfold hide.
+intros n H H'.
+(* H is displayed as (forall n, n=0) *)
+apply H with (n:=n).
+Undo.
+(* H' is displayed as (forall n0, n=n0) *)
+apply H' with (n0:=0).
+Qed.