From c61b48f8b123e572b33c6d080a2b09aa5ecde979 Mon Sep 17 00:00:00 2001
From: notin
Date: Fri, 1 Feb 2008 19:22:41 +0000
Subject: Ajout de 2 tests

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10499 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/bugs/closed/1519.v | 23 +++++++++++++++++++++++
 test-suite/bugs/opened/1773.v | 10 ++++++++++
 2 files changed, 33 insertions(+)
 create mode 100644 test-suite/bugs/closed/1519.v
 create mode 100644 test-suite/bugs/opened/1773.v

diff --git a/test-suite/bugs/closed/1519.v b/test-suite/bugs/closed/1519.v
new file mode 100644
index 0000000000..98e3e2144c
--- /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.
diff --git a/test-suite/bugs/opened/1773.v b/test-suite/bugs/opened/1773.v
new file mode 100644
index 0000000000..4aabf19c98
--- /dev/null
+++ b/test-suite/bugs/opened/1773.v
@@ -0,0 +1,10 @@
+Goal forall B C : nat -> nat -> Prop, forall k, C 0 k ->
+  (exists A, (forall k', C A k' -> B A k') -> B A k).
+Proof.
+  intros B C k H.
+  econstructor.
+  intros X.
+  apply X.
+  apply H.
+Qed.
+
-- 
cgit v1.2.3