Removing test for opened bugs that were already present in the closed test-suite.

8 files changed, 0 insertions, 129 deletions

diff --git a/test-suite/bugs/opened/3045.v b/test-suite/bugs/opened/3045.v
deleted file mode 100644
index b7f40b4ad..000000000
--- a/test-suite/bugs/opened/3045.v
+++ /dev/null
@@ -1,30 +0,0 @@
-Set Asymmetric Patterns.
-Generalizable All Variables.
-Set Implicit Arguments.
-Set Universe Polymorphism.
-
-Record SpecializedCategory (obj : Type) :=
-  {
-    Object :> _ := obj;
-    Morphism : obj -> obj -> Type;
-
-    Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
-  }.
-
-Arguments Compose {obj} [C s d d'] m1 m2 : rename.
-
-Inductive ReifiedMorphism : forall objC (C : SpecializedCategory objC), C -> C -> Type :=
-| ReifiedComposedMorphism : forall objC C s d d', ReifiedMorphism C d d' -> ReifiedMorphism C s d -> @ReifiedMorphism objC C s d'.
-
-Fixpoint ReifiedMorphismDenote objC C s d (m : @ReifiedMorphism objC C s d) : Morphism C s d :=
-  match m in @ReifiedMorphism objC C s d return Morphism C s d with
-    | ReifiedComposedMorphism _ _ _ _ _ m1 m2 => Compose (@ReifiedMorphismDenote _ _ _ _ m1)
-                                                         (@ReifiedMorphismDenote _ _ _ _ m2)
-  end.
-
-Fixpoint ReifiedMorphismSimplifyWithProof objC C s d (m : @ReifiedMorphism objC C s d)
-: { m' : ReifiedMorphism C s d | ReifiedMorphismDenote m = ReifiedMorphismDenote m' }.
-refine match m with
-         | ReifiedComposedMorphism _ _ s0 d0 d0' m1 m2 => _
-       end; clear m.
-Fail destruct (@ReifiedMorphismSimplifyWithProof _ _ _ _ m1) as [ [] ? ].
diff --git a/test-suite/bugs/opened/3326.v b/test-suite/bugs/opened/3326.v
deleted file mode 100644
index f73117a2e..000000000
--- a/test-suite/bugs/opened/3326.v
+++ /dev/null
@@ -1,18 +0,0 @@
-Class ORDER A := Order {
-  LEQ : A -> A -> bool;
-  leqRefl: forall x, true = LEQ x x
-}.
-
-Section XXX.
-
-Variable A:Type.
-Variable (O:ORDER A).
-Definition aLeqRefl := @leqRefl _ O.
-
-Lemma OK : forall x, true = LEQ x x.
-  intros.
-  unfold LEQ.
-  destruct O.
-  clear.
-  Fail apply aLeqRefl. (* Toplevel input, characters 15-30:
-Anomaly: Uncaught exception Not_found(_). Please report. *)
diff --git a/test-suite/bugs/opened/3562.v b/test-suite/bugs/opened/3562.v
deleted file mode 100644
index 04a1223b6..000000000
--- a/test-suite/bugs/opened/3562.v
+++ /dev/null
@@ -1,2 +0,0 @@
-Theorem t: True.
-Fail destruct 0 as x.
diff --git a/test-suite/bugs/opened/3657.v b/test-suite/bugs/opened/3657.v
deleted file mode 100644
index 6faec0765..000000000
--- a/test-suite/bugs/opened/3657.v
+++ /dev/null
@@ -1,33 +0,0 @@
-(* Set Primitive Projections. *)
-Class foo {A} {a : A} := { bar := a; baz : bar = bar }.
-Arguments bar {_} _ {_}.
-Instance: forall A a, @foo A a.
-intros; constructor.
-abstract reflexivity.
-Defined.
-Goal @bar _ Set _ = (@bar _ (fun _ : Set => Set) _) nat.
-Proof.
-  Check (bar Set).
-  Check (bar (fun _ : Set => Set)).
-  Fail change (bar (fun _ : Set => Set)) with (bar Set). (* Error: Conversion test raised an anomaly *)
-
-Abort.
-
-
-Module A.
-Universes i j.
-Constraint i < j.
-Variable  foo : Type@{i}.
-Goal Type@{i}.
-  Fail let t := constr:(Type@{j}) in
-  change Type with t.
-Abort.
-
-Goal Type@{j}.
-  Fail let t := constr:(Type@{i}) in
-  change Type with t.
-  let t := constr:(Type@{i}) in
-  change t. exact foo.
-Defined.
-
-End A.
diff --git a/test-suite/bugs/opened/3670.v b/test-suite/bugs/opened/3670.v
deleted file mode 100644
index cf5e9b090..000000000
--- a/test-suite/bugs/opened/3670.v
+++ /dev/null
@@ -1,19 +0,0 @@
-Module Type FOO.
-  Parameters P Q : Type -> Type.
-End FOO.
-
-Module Type BAR.
-  Declare Module Export foo : FOO.
-  Parameter f : forall A, P A -> Q A -> A.
-End BAR.
-
-Module Type BAZ.
-  Declare Module Export foo : FOO.
-  Parameter g : forall A, P A -> Q A -> A.
-End BAZ.
-
-Module BAR_FROM_BAZ (baz : BAZ) : BAR.
-  Import baz.
-  Module foo <: FOO := foo.
-  Definition f : forall A, P A -> Q A -> A := g.
-End BAR_FROM_BAZ.
diff --git a/test-suite/bugs/opened/3675.v b/test-suite/bugs/opened/3675.v
deleted file mode 100644
index 93227ab85..000000000
--- a/test-suite/bugs/opened/3675.v
+++ /dev/null
@@ -1,20 +0,0 @@
-Set Primitive Projections.
-Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
-Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
-Arguments idpath {A a} , [A] a.
-Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := match p, q with idpath, idpath => idpath end.
-Notation "p @ q" := (concat p q) (at level 20) : path_scope.
-Axiom ap : forall {A B:Type} (f:A -> B) {x y:A} (p:x = y), f x = f y.
-Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := forall x : A, r (s x) = x.
-Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A ; eisretr : forall x, f (equiv_inv x) = x }.
-Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope.
-Local Open Scope path_scope.
-Local Open Scope equiv_scope.
-Generalizable Variables A B C f g.
-Lemma isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g}
-: IsEquiv (compose g f).
-Proof.
-  refine (Build_IsEquiv A C
-                        (compose g f)
-                        (compose f^-1 g^-1) _).
-  exact (fun c => ap g (@eisretr _ _ f _ (g^-1 c)) @ (@eisretr _ _ g _ c)).
diff --git a/test-suite/bugs/opened/3788.v b/test-suite/bugs/opened/3788.v
deleted file mode 100644
index 8e605a00f..000000000
--- a/test-suite/bugs/opened/3788.v
+++ /dev/null
@@ -1,5 +0,0 @@
-Set Implicit Arguments.
-Global Set Primitive Projections.
-Record Functor (C D : Type) := { object_of :> forall _ : C, D }.
-Axiom path_functor_uncurried : forall C D (F G : Functor C D) (_ : sigT (fun HO : object_of F = object_of G => Set)), F = G.
-Fail Lemma path_functor_uncurried_snd C D F G HO HM : (@path_functor_uncurried C D F G (existT _ HO HM)) = HM.
diff --git a/test-suite/bugs/opened/3808.v b/test-suite/bugs/opened/3808.v
deleted file mode 100644
index df40ca191..000000000
--- a/test-suite/bugs/opened/3808.v
+++ /dev/null
@@ -1,2 +0,0 @@
-Inductive Foo : (let enforce := (fun x => x) : Type@{j} -> Type@{i} in Type@{i})
-  := foo : Foo.