3 files changed, 2 insertions, 35 deletions
diff --git a/test-suite/bugs/opened/3461.v b/test-suite/bugs/opened/3461.v
index 1ca05a743f..1b625e6a15 100644
--- a/test-suite/bugs/opened/3461.v
+++ b/test-suite/bugs/opened/3461.v
@@ -1,4 +1,5 @@
 Lemma foo (b : bool) :
   exists x : nat, x = x.
 Proof.
-eexists; Fail eexact (eq_refl b).
+eexists. 
+Fail eexact (eq_refl b).
diff --git a/test-suite/bugs/opened/3625.v b/test-suite/bugs/opened/3625.v
deleted file mode 100644
index 46a6c009eb..0000000000
--- a/test-suite/bugs/opened/3625.v
+++ /dev/null
@@ -1,7 +0,0 @@
-Set Implicit Arguments.
-Set Primitive Projections.
-Record prod A B := pair { fst : A ; snd : B }.
-
-Fail Goal forall x y : prod Set Set, x.(@fst) = y.(@fst).
-(*  intros.
-    apply f_equal. *)
diff --git a/test-suite/bugs/opened/3660.v b/test-suite/bugs/opened/3660.v
deleted file mode 100644
index ed8964ce11..0000000000
--- a/test-suite/bugs/opened/3660.v
+++ /dev/null
@@ -1,27 +0,0 @@
-Generalizable All Variables.
-Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
-Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope.
-Open Scope function_scope.
-Axiom ap : forall {A B:Type} (f:A -> B) {x y:A} (p:x = y), f x = f y.
-Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A }.
-Record Equiv A B := { equiv_fun :> A -> B ; equiv_isequiv :> IsEquiv equiv_fun }.
-Notation "A <~> B" := (Equiv A B) (at level 85) : equiv_scope.
-Axiom IsHSet : Type -> Type.
-Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g} : IsEquiv (compose g f) | 1000.
-admit.
-Defined.
-Set Primitive Projections.
-Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
-Canonical Structure default_HSet:= fun T P => (@BuildhSet T P).
-Global Instance isequiv_ap_setT X Y : IsEquiv (@ap _ _ setT X Y).
-admit.
-Defined.
-Local Open Scope equiv_scope.
-Axiom equiv_path : forall (A B : Type) (p : A = B), A <~> B.
-
-Goal forall (C D : hSet), IsEquiv (fun x : C = D => (equiv_path C D (ap setT x))).
-  intros.
-  change (IsEquiv (equiv_path C D o @ap _ _ setT C D)).
-  apply @isequiv_compose; [ | admit ].
-  Set Typeclasses Debug. 
-  typeclasses eauto.