Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg

6 files changed, 41 insertions, 3 deletions

diff --git a/test-suite/bugs/closed/2319.v b/test-suite/bugs/closed/2319.v
new file mode 100644
index 00000000..e06fb975
--- /dev/null
+++ b/test-suite/bugs/closed/2319.v
@@ -0,0 +1,13 @@
+Section S.
+
+  CoInductive A (X: Type) := mkA: A X -> A X.
+  Variable T : Type.
+
+  (* This used to loop (bug #2319) *)
+  Timeout 5 Eval vm_compute in cofix s : A T := mkA T s.
+
+  CoFixpoint s : A T := mkA T s
+        with t : A unit := mkA unit (mkA unit t).
+  Timeout 5 Eval vm_compute in s.
+
+End S.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/1507.v b/test-suite/bugs/closed/shouldsucceed/1507.v
index f1872a2b..ea72ba89 100644
--- a/test-suite/bugs/closed/shouldsucceed/1507.v
+++ b/test-suite/bugs/closed/shouldsucceed/1507.v
@@ -2,7 +2,7 @@
    Implementing reals a la Stolzenberg
 
    Danko Ilik, March 2007
-   svn revision: $Id$
+   svn revision: $Id: 1507.v 12337 2009-09-17 15:58:14Z glondu $
 
    XField.v -- (unfinished) axiomatisation of the theories of real and
                rational intervals.
diff --git a/test-suite/bugs/closed/shouldsucceed/2145.v b/test-suite/bugs/closed/shouldsucceed/2145.v
index b6c5da65..4dc0de74 100644
--- a/test-suite/bugs/closed/shouldsucceed/2145.v
+++ b/test-suite/bugs/closed/shouldsucceed/2145.v
@@ -1,7 +1,7 @@
 (* Test robustness of Groebner tactic in presence of disequalities *)
 
 Require Export Reals.
-Require Export NsatzR.
+Require Export Nsatz.
 
 Open Scope R_scope.
 
@@ -15,6 +15,6 @@ Lemma essai :
 Proof.
 intros.
 (* clear H. groebner used not to work when H was not cleared *)
-nsatzR.
+nsatz.
 Qed.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/2262.v b/test-suite/bugs/closed/shouldsucceed/2262.v
new file mode 100644
index 00000000..b61f18b8
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2262.v
@@ -0,0 +1,11 @@
+
+
+Generalizable Variables A.
+Class Test A := { test : A }.
+
+Lemma mylemma : forall `{Test A}, test = test.
+Admitted. (* works fine *)
+
+Definition mylemma' := forall `{Test A}, test = test.
+About mylemma'.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2303.v b/test-suite/bugs/closed/shouldsucceed/2303.v
new file mode 100644
index 00000000..e614b9b5
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2303.v
@@ -0,0 +1,4 @@
+Class A := a: unit.
+Class B (x: unit).
+Axiom H: forall x: A, @B x -> x = x -> unit.
+Definition Field (z: A) (m: @B z) x := (@H _ _ x) = z.
diff --git a/test-suite/bugs/closed/shouldsucceed/2347.v b/test-suite/bugs/closed/shouldsucceed/2347.v
new file mode 100644
index 00000000..e433f158
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2347.v
@@ -0,0 +1,10 @@
+Require Import EquivDec List.
+Generalizable All Variables.
+
+Program Definition list_eqdec `(eqa : EqDec A eq) : EqDec (list A) eq := 
+ (fun (x y : list A) => _).
+Admit Obligations of list_eqdec.
+
+Program Definition list_eqdec' `(eqa : EqDec A eq) : EqDec (list A) eq :=
+  (fun _ : nat => (fun (x y : list A) => _)) 0.
+Admit Obligations of list_eqdec'.