Add missing test-suite files for closed bugs.

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

4 files changed, 28 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/1900.v b/test-suite/bugs/closed/shouldsucceed/1900.v
new file mode 100644
index 000000000..cf03efda4
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1900.v
@@ -0,0 +1,8 @@
+Parameter A : Type .
+
+Definition eq_A := @eq A.
+
+Goal forall x, eq_A x x.
+intros.
+reflexivity.
+Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/1901.v b/test-suite/bugs/closed/shouldsucceed/1901.v
new file mode 100644
index 000000000..598db3660
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1901.v
@@ -0,0 +1,11 @@
+Require Import Relations.
+
+Record Poset{A:Type}(Le : relation A) : Type :=
+  Build_Poset
+  { 
+    Le_refl : forall x : A, Le x x; 
+    Le_trans : forall x y z : A, Le x y -> Le y z -> Le x z; 
+    Le_antisym : forall x y : A, Le x y -> Le y x -> x = y }.
+
+Definition nat_Poset : Poset Peano.le.
+Admitted.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/1977.v b/test-suite/bugs/closed/shouldsucceed/1977.v
new file mode 100644
index 000000000..28715040c
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1977.v
@@ -0,0 +1,4 @@
+Inductive T {A} : Prop := c : A -> T.
+Goal (@T nat).
+apply c. exact 0.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1981.v b/test-suite/bugs/closed/shouldsucceed/1981.v
new file mode 100644
index 000000000..0c3b96dad
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1981.v
@@ -0,0 +1,5 @@
+Implicit Arguments ex_intro [A].
+
+Goal exists n : nat, True.
+  eapply ex_intro. exact 0. exact I. 
+Qed.