summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-08-06 16:15:08 -0400
committerGravatar Stephane Glondu <steph@glondu.net>2010-08-06 16:17:55 -0400
commitf18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (patch)
treec413c5bb42d20daf5307634ae6402526bb994fd6 /test-suite/bugs/closed
parentb9f47391f7f259c24119d1de0a87839e2cc5e80c (diff)
Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg
Diffstat (limited to 'test-suite/bugs/closed')
-rw-r--r--test-suite/bugs/closed/2319.v13
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1507.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2145.v4
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2262.v11
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2303.v4
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2347.v10
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'.