Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

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 00000000..98e3e214
--- /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.