Ajout de 2 tests

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10499 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 23 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/1519.v b/test-suite/bugs/closed/1519.v
new file mode 100644
index 000000000..98e3e2144
--- /dev/null
+++ b/test-suite/bugs/closed/1519.v
@@ -0,0 +1,23 @@
+Section S.
+
+  Variable A:Prop.
+  Variable W:A.
+  
+  Remark T: A -> A.
+    intro Z.
+    rename W into Z_.
+    rename Z into W.
+    rename Z_ into Z.
+    exact Z.
+  Qed.
+
+  (* bug :
+     Error:
+     Unbound reference: In environment
+     A : Prop
+     W : A
+     Z : A
+     The reference 2 is free
+     *)
+
+End S.