21 files changed, 57 insertions, 561 deletions
diff --git a/test-suite/bugs/opened/1501.v b/test-suite/bugs/opened/1501.v
deleted file mode 100644
index b36f21da..00000000
--- a/test-suite/bugs/opened/1501.v
+++ /dev/null
@@ -1,96 +0,0 @@
-Set Implicit Arguments.
-
-
-Require Export Relation_Definitions.
-Require Export Setoid.
-
-
-Section Essais.
-
-(* Parametrized Setoid *)
-Parameter K : Type -> Type.
-Parameter equiv : forall A : Type, K A -> K A -> Prop.
-Parameter equiv_refl : forall (A : Type) (x : K A), equiv x x.
-Parameter equiv_sym : forall (A : Type) (x y : K A), equiv x y -> equiv y x.
-Parameter equiv_trans : forall (A : Type) (x y z : K A), equiv x y -> equiv y z
--> equiv x z.
-
-(* basic operations *)
-Parameter val : forall A : Type, A -> K A.
-Parameter bind : forall A B : Type, K A -> (A -> K B) -> K B.
-
-Parameter
-  bind_compat :
-    forall (A B : Type) (m1 m2 : K A) (f1 f2 : A -> K B),
-    equiv m1 m2 ->
-    (forall x : A, equiv (f1 x) (f2 x)) -> equiv (bind m1 f1) (bind m2 f2).
-
-(* monad axioms *)
-Parameter
-  bind_val_l :
-    forall (A B : Type) (a : A) (f : A -> K B), equiv (bind (val a) f) (f a).
-Parameter
-  bind_val_r :
-    forall (A : Type) (m : K A), equiv (bind m (fun a => val a)) m.
-Parameter
-  bind_assoc :
-    forall (A B C : Type) (m : K A) (f : A -> K B) (g : B -> K C),
-    equiv (bind (bind m f) g) (bind m (fun a => bind (f a) g)).
-
-
-Hint Resolve equiv_refl equiv_sym equiv_trans: monad.
-
-Instance equiv_rel A: Equivalence (@equiv A).
-Proof.
- constructor.
- intros xa; apply equiv_refl.
- intros xa xb; apply equiv_sym.
- intros xa xb xc; apply equiv_trans.
-Defined.
-
-Definition fequiv (A B: Type)  (f g: A -> K B) := forall (x:A), (equiv (f x) (g
-x)).
-
-Lemma fequiv_refl : forall (A B: Type) (f : A -> K B), fequiv f f.
-Proof.
-  unfold fequiv; auto with monad.
-Qed.
-
-Lemma fequiv_sym : forall (A B: Type) (x y : A -> K B), fequiv x y -> fequiv y
-x.
-Proof.
-  unfold fequiv; auto with monad.
-Qed.
-
-Lemma fequiv_trans : forall (A B: Type) (x y z : A -> K B), fequiv x y ->
-fequiv
-y z -> fequiv x z.
-Proof.
-  unfold fequiv; intros; eapply equiv_trans; auto with monad.
-Qed.
-
-Instance fequiv_re A B: Equivalence (@fequiv A B).
-Proof.
- constructor.
- intros f; apply fequiv_refl.
- intros f g; apply fequiv_sym.
- intros f g h; apply fequiv_trans.
-Defined.
-
-Instance bind_mor A B: Morphisms.Proper (@equiv _ ==> @fequiv _ _ ==> @equiv _) (@bind A B).
-Proof.
- unfold fequiv; intros x y xy_equiv f g fg_equiv; apply bind_compat; auto.
-Qed.
-
-Lemma test:
-  forall (A B: Type) (m1 m2 m3: K A) (f: A -> A -> K B),
- (equiv m1 m2) -> (equiv m2 m3) ->
-   equiv (bind m1 (fun a => bind m2 (fun a' => f a a')))
-         (bind m2 (fun a => bind m3 (fun a' => f a a'))).
-Proof.
-  intros A B m1 m2 m3 f H1 H2.
-  setoid_rewrite H1. (* this works *)
-  Fail setoid_rewrite H2.
-Abort.
-(*  trivial by equiv_refl.
-Qed.*)
diff --git a/test-suite/bugs/opened/1596.v b/test-suite/bugs/opened/1596.v
index 7c5dc416..820022d9 100644
--- a/test-suite/bugs/opened/1596.v
+++ b/test-suite/bugs/opened/1596.v
@@ -2,7 +2,6 @@ Require Import Relations.
 Require Import FSets.
 Require Import Arith.
 Require Import Omega.
-Unset Standard Proposition Elimination Names.
 
 Set Keyed Unification.
 
@@ -258,4 +257,4 @@ n).
     apply SynInc;apply H.mem_2;trivial.
     rewrite H in H0. discriminate. (* !! impossible here !! *)
   Qed.
-End B.
-\ No newline at end of file
+End B.
diff --git a/test-suite/bugs/opened/743.v b/test-suite/bugs/opened/1615.v
index 28257014..28257014 100644
--- a/test-suite/bugs/opened/743.v
+++ b/test-suite/bugs/opened/1615.v
diff --git a/test-suite/bugs/opened/1811.v b/test-suite/bugs/opened/1811.v
index 10c988fc..57c17443 100644
--- a/test-suite/bugs/opened/1811.v
+++ b/test-suite/bugs/opened/1811.v
@@ -7,4 +7,4 @@ Goal forall b1 b2, (negb b1 = b2)  ->  xorb true b1 = b2.
 Proof.
   intros b1 b2.
   Fail rewrite neg2xor.
-Abort.
-\ No newline at end of file
+Abort.
diff --git a/test-suite/bugs/opened/2456.v b/test-suite/bugs/opened/2456.v
deleted file mode 100644
index 6cca5c9f..00000000
--- a/test-suite/bugs/opened/2456.v
+++ /dev/null
@@ -1,53 +0,0 @@
-
-Require Import Equality.
-
-Parameter Patch : nat -> nat -> Set.
-
-Inductive Catch (from to : nat) : Type
-    := MkCatch : forall (p : Patch from to),
-                 Catch from to.
-Implicit Arguments MkCatch [from to].
-
-Inductive CatchCommute5
-        : forall {from mid1 mid2 to : nat},
-          Catch from mid1
-       -> Catch mid1 to
-       -> Catch from mid2
-       -> Catch mid2 to
-       -> Prop
-     := MkCatchCommute5 :
-           forall {from mid1 mid2 to : nat}
-                  (p : Patch from mid1)
-                  (q : Patch mid1 to)
-                  (q' : Patch from mid2)
-                  (p' : Patch mid2 to),
-           CatchCommute5 (MkCatch p) (MkCatch q) (MkCatch q') (MkCatch p').
-
-Inductive CatchCommute {from mid1 mid2 to : nat}
-                       (p : Catch from mid1)
-                       (q : Catch mid1 to)
-                       (q' : Catch from mid2)
-                       (p' : Catch mid2 to)
-                     : Prop
-    := isCatchCommute5 : forall (catchCommuteDetails : CatchCommute5 p q q' p'),
-                         CatchCommute p q q' p'.
-Notation "<< p , q >> <~> << q' , p' >>"
-    := (CatchCommute p q q' p')
-    (at level 60, no associativity).
-
-Lemma CatchCommuteUnique2 :
-      forall {from mid mid' to : nat}
-             {p   : Catch from mid}  {q   : Catch mid  to}
-             {q'  : Catch from mid'} {p'  : Catch mid' to}
-             {q'' : Catch from mid'} {p'' : Catch mid' to}
-             (commute1 : <<p, q>> <~> <<q', p'>>)
-             (commute2 : <<p, q>> <~> <<q'', p''>>),
-      (p' = p'') /\ (q' = q'').
-Proof with auto.
-intros.
-set (X := commute2).
-Fail dependent destruction commute1;
-dependent destruction catchCommuteDetails;
-dependent destruction commute2;
-dependent destruction catchCommuteDetails generalizing X.
-Admitted.
diff --git a/test-suite/bugs/opened/2814.v b/test-suite/bugs/opened/2814.v
deleted file mode 100644
index a740b438..00000000
--- a/test-suite/bugs/opened/2814.v
+++ /dev/null
@@ -1,5 +0,0 @@
-Require Import Program.
-
-Goal forall (x : Type) (f g : Type -> Type) (H : f x ~= g x), False.
-  intros.
-  Fail induction H.
diff --git a/test-suite/bugs/opened/3100.v b/test-suite/bugs/opened/3100.v
deleted file mode 100644
index 6f35a74d..00000000
--- a/test-suite/bugs/opened/3100.v
+++ /dev/null
@@ -1,9 +0,0 @@
-Fixpoint F (n : nat) (A : Type) : Type :=
-  match n with
-  | 0 => True
-  | S n => forall (x : A), F n (x = x)
-  end.
-
-Goal forall A n, (forall (x : A) (e : x = x), F n (e = e)).
-intros A n.
-Fail change (forall x, F n (x = x)) with (F (S n)).
diff --git a/test-suite/bugs/opened/3209.v b/test-suite/bugs/opened/3209.v
deleted file mode 100644
index 3203afa1..00000000
--- a/test-suite/bugs/opened/3209.v
+++ /dev/null
@@ -1,17 +0,0 @@
-Inductive eqT {A} (x : A) : A -> Type :=
-  reflT : eqT x x.
-Definition Bi_inv (A B : Type) (f : (A -> B)) :=
-  sigT (fun (g : B -> A) =>
-          sigT (fun (h : B -> A) =>
-                  sigT (fun (α : forall b : B, eqT (f (g b)) b) =>
-                          forall a : A, eqT (h (f a)) a))).
-Definition TEquiv (A B : Type) := sigT (fun (f : A -> B) => Bi_inv _ _ f).
-
-Axiom UA : forall (A B : Type), TEquiv (TEquiv A B) (eqT A B).
-Definition idtoeqv {A B} (e : eqT A B) : TEquiv A B :=
-  sigT_rect (fun _ => TEquiv A B)
-            (fun (f : TEquiv A B -> eqT A B) H =>
-               sigT_rect (fun _ => TEquiv A B)
-                         (fun g _ => g e)
-                         H)
-            (UA A B).
diff --git a/test-suite/bugs/opened/3230.v b/test-suite/bugs/opened/3230.v
deleted file mode 100644
index 265310b1..00000000
--- a/test-suite/bugs/opened/3230.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Structure type : Type := Pack { ob : Type }.
-Polymorphic Record category := { foo : Type }.
-Definition FuncComp := Pack category.
-Axiom C : category.
-
-Check (C : ob FuncComp). (* OK *)
-
-Canonical Structure FuncComp.
-
-Check (C : ob FuncComp).
-(* Toplevel input, characters 15-39:
-Error:
-The term "C" has type "category" while it is expected to have type
- "ob FuncComp". *)
diff --git a/test-suite/bugs/opened/3263.v b/test-suite/bugs/opened/3263.v
deleted file mode 100644
index f0c707bd..00000000
--- a/test-suite/bugs/opened/3263.v
+++ /dev/null
@@ -1,232 +0,0 @@
-Require Import TestSuite.admit.
-(* File reduced by coq-bug-finder from originally 10918 lines, then 3649 lines to 3177 lines, then from 3189 lines to 3164 lines, then from 2653 lines to 2496 lines,  2653 lines, then from 1642 lines to 651 lines, then from 736 lines to 473 lines, then from 433 lines to 275 lines, then from 258 lines to 235 lines. *)
-Generalizable All Variables.
-Set Implicit Arguments.
-
-Arguments fst {_ _} _.
-Arguments snd {_ _} _.
-
-Axiom cheat : forall {T}, T.
-
-Reserved Notation "g 'o' f" (at level 40, left associativity).
-
-Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
-Arguments idpath {A a} , [A] a.
-Notation "x = y" := (paths x y) : type_scope.
-
-Definition symmetry {A : Type} {x y : A} (p : x = y) : y = x
-  := match p with idpath => idpath end.
-
-Delimit Scope morphism_scope with morphism.
-Delimit Scope category_scope with category.
-Delimit Scope object_scope with object.
-Record PreCategory (object : Type) :=
-  Build_PreCategory' {
-      object :> Type := object;
-      morphism : object -> object -> Type;
-      identity : forall x, morphism x x;
-      compose : forall s d d',
-                  morphism d d'
-                  -> morphism s d
-                  -> morphism s d'
-                              where "f 'o' g" := (compose f g);
-      associativity : forall x1 x2 x3 x4
-                             (m1 : morphism x1 x2)
-                             (m2 : morphism x2 x3)
-                             (m3 : morphism x3 x4),
-                        (m3 o m2) o m1 = m3 o (m2 o m1);
-      associativity_sym : forall x1 x2 x3 x4
-                                 (m1 : morphism x1 x2)
-                                 (m2 : morphism x2 x3)
-                                 (m3 : morphism x3 x4),
-                            m3 o (m2 o m1) = (m3 o m2) o m1;
-      left_identity : forall a b (f : morphism a b), identity b o f = f;
-      right_identity : forall a b (f : morphism a b), f o identity a = f;
-      identity_identity : forall x, identity x o identity x = identity x
-    }.
-Bind Scope category_scope with PreCategory.
-Arguments PreCategory {_}.
-Arguments identity {_} [!C%category] x%object : rename.
-
-Arguments compose {_} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename.
-
-Infix "o" := compose : morphism_scope.
-
-Delimit Scope functor_scope with functor.
-Local Open Scope morphism_scope.
-Record Functor `(C : @PreCategory objC, D : @PreCategory objD) :=
-  {
-    object_of :> C -> D;
-    morphism_of : forall s d, morphism C s d
-                              -> morphism D (object_of s) (object_of d);
-    composition_of : forall s d d'
-                            (m1 : morphism C s d) (m2: morphism C d d'),
-                       morphism_of _ _ (m2 o m1)
-                       = (morphism_of _ _ m2) o (morphism_of _ _ m1);
-    identity_of : forall x, morphism_of _ _ (identity x)
-                            = identity (object_of x)
-  }.
-Bind Scope functor_scope with Functor.
-
-Arguments morphism_of {_} [C%category] {_} [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch.
-
-Notation "F '_1' m" := (morphism_of F m) (at level 10, no associativity) : morphism_scope.
-
-Class IsIsomorphism `{C : @PreCategory objC} {s d} (m : morphism C s d) :=
-  {
-    morphism_inverse : morphism C d s;
-    left_inverse : morphism_inverse o m = identity _;
-    right_inverse : m o morphism_inverse = identity _
-  }.
-
-Definition opposite `(C : @PreCategory objC) : PreCategory
-  := @Build_PreCategory'
-       C
-       (fun s d => morphism C d s)
-       (identity (C := C))
-       (fun _ _ _ m1 m2 => m2 o m1)
-       (fun _ _ _ _ _ _ _ => @associativity_sym _ _ _ _ _ _ _ _ _)
-       (fun _ _ _ _ _ _ _ => @associativity _ _ _ _ _ _ _ _ _)
-       (fun _ _ => @right_identity _ _ _ _)
-       (fun _ _ => @left_identity _ _ _ _)
-       (@identity_identity _ C).
-
-Notation "C ^op" := (opposite C) (at level 3) : category_scope.
-
-Definition prod `(C : @PreCategory objC, D : @PreCategory objD) : @PreCategory (objC * objD).
-  refine (@Build_PreCategory'
-            (C * D)%type
-            (fun s d => (morphism C (fst s) (fst d)
-                         * morphism D (snd s) (snd d))%type)
-            (fun x => (identity (fst x), identity (snd x)))
-            (fun s d d' m2 m1 => (fst m2 o fst m1, snd m2 o snd m1))
-            _
-            _
-            _
-            _
-            _); admit.
-Defined.
-Infix "*" := prod : category_scope.
-
-Definition compose_functor `(C : @PreCategory objC, D : @PreCategory objD, E : @PreCategory objE) (G : Functor D E) (F : Functor C D) : Functor C E
-  := Build_Functor
-       C E
-       (fun c => G (F c))
-       (fun _ _ m => morphism_of G (morphism_of F m))
-       cheat
-       cheat.
-
-Infix "o" := compose_functor : functor_scope.
-
-Record NaturalTransformation `(C : @PreCategory objC, D : @PreCategory objD) (F G : Functor C D) :=
-  Build_NaturalTransformation' {
-      components_of :> forall c, morphism D (F c) (G c);
-      commutes : forall s d (m : morphism C s d),
-                   components_of d o F _1 m = G _1 m o components_of s;
-
-      commutes_sym : forall s d (m : C.(morphism) s d),
-                       G _1 m o components_of s = components_of d o F _1 m
-    }.
-Definition functor_category `(C : @PreCategory objC, D : @PreCategory objD) : PreCategory
-  := @Build_PreCategory' (Functor C D)
-                         (@NaturalTransformation _ C _ D)
-                         cheat
-                         cheat
-                         cheat
-                         cheat
-                         cheat
-                         cheat
-                         cheat.
-
-Definition opposite_functor `(F : @Functor objC C objD D) : Functor C^op D^op
-  := Build_Functor (C^op) (D^op)
-                   (object_of F)
-                   (fun s d => morphism_of F (s := d) (d := s))
-                   (fun d' d s m1 m2 => composition_of F s d d' m2 m1)
-                   (identity_of F).
-
-Definition opposite_invL `(F : @Functor objC C^op objD D) : Functor C D^op
-  := Build_Functor C (D^op)
-                   (object_of F)
-                   (fun s d => morphism_of F (s := d) (d := s))
-                   (fun d' d s m1 m2 => composition_of F s d d' m2 m1)
-                   (identity_of F).
-Notation "F ^op" := (opposite_functor F) : functor_scope.
-
-Notation "F ^op'L" := (opposite_invL F) (at level 3) : functor_scope.
-Definition fst `{C : @PreCategory objC, D : @PreCategory objD} : Functor (C * D) C
-  := Build_Functor (C * D) C
-                   (@fst _ _)
-                   (fun _ _ => @fst _ _)
-                   (fun _ _ _ _ _ => idpath)
-                   (fun _ => idpath).
-
-Definition snd `{C : @PreCategory objC, D : @PreCategory objD} : Functor (C * D) D
-  := Build_Functor (C * D) D
-                   (@snd _ _)
-                   (fun _ _ => @snd _ _)
-                   (fun _ _ _ _ _ => idpath)
-                   (fun _ => idpath).
-Definition prod_functor `(F : @Functor objC C objD D, F' : @Functor objC C objD' D')
-: Functor C (D * D')
-  := Build_Functor
-       C (D * D')
-       (fun c => (F c, F' c))
-       (fun s d m => (F _1 m, F' _1 m))%morphism
-       cheat
-       cheat.
-Definition pair `(F : @Functor objC C objD D, F' : @Functor objC' C' objD' D') : Functor (C * C') (D * D')
-  := (prod_functor (F o fst) (F' o snd))%functor.
-Notation cat_of obj :=
-  (@Build_PreCategory' obj
-                       (fun x y => forall _ : x, y)
-                       (fun _ x => x)
-                       (fun _ _ _ f g x => f (g x))%core
-                       (fun _ _ _ _ _ _ _ => idpath)
-                       (fun _ _ _ _ _ _ _ => idpath)
-                       (fun _ _ _ => idpath)
-                       (fun _ _ _ => idpath)
-                       (fun _ => idpath)).
-
-Definition hom_functor `(C : @PreCategory objC) : Functor (C^op * C) (cat_of Type)
-  := Build_Functor _ _ cheat cheat cheat cheat.
-
-Definition induced_hom_natural_transformation `(F : @Functor objC C objD D)
-: NaturalTransformation (hom_functor C) (hom_functor D o pair F^op F)
-  := Build_NaturalTransformation' _ _ cheat cheat cheat.
-
-Class IsFullyFaithful `(F : @Functor objC C objD D)
-  := is_fully_faithful
-     : forall x y : C,
-         IsIsomorphism (induced_hom_natural_transformation F (x, y)).
-
-Definition coyoneda `(A : @PreCategory objA) : Functor A^op (@functor_category _ A _ (cat_of Type))
-  := cheat.
-
-Definition yoneda `(A : @PreCategory objA) : Functor A (@functor_category _ A^op _ (cat_of Type))
-  := (((coyoneda A^op)^op'L)^op'L)%functor.
-Definition coyoneda_embedding `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@coyoneda _ A).
-Admitted.
-
-Definition yoneda_embedding_fast `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@yoneda _ A).
-Proof.
-  intros a b.
-  pose proof (coyoneda_embedding A^op a b) as CYE.
-  unfold yoneda.
-  Time let t := (type of CYE) in
-  let t' := (eval simpl in t) in pose proof ((fun (x : t) => (x : t')) CYE) as CYE'. (* Finished transaction in 0. secs (0.216013u,0.004s) *)
-  Fail Timeout 1 let t := match goal with |- ?G => constr:(G) end in
-  let t' := (eval simpl in t) in exact ((fun (x : t') => (x : t)) CYE').
-  Time let t := match goal with |- ?G => constr:(G) end in
-  let t' := (eval simpl in t) in exact ((fun (x : t') => (x : t)) CYE'). (* Finished transaction in 0. secs (0.248016u,0.s) *)
-Fail Timeout 2 Defined.
-Time Defined. (* Finished transaction in 1. secs (0.432027u,0.s) *)
-
-Definition yoneda_embedding `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@yoneda _ A).
-Proof.
-  intros a b.
-  pose proof (coyoneda_embedding A^op a b) as CYE.
-  unfold yoneda; simpl in *.
-  Fail Timeout 1 exact CYE.
-  Time exact CYE. (* Finished transaction in 0. secs (0.012001u,0.s) *)
-Fail Timeout 60 Defined. (* Timeout! *)
diff --git a/test-suite/bugs/opened/3320.v b/test-suite/bugs/opened/3320.v
deleted file mode 100644
index 05cf7328..00000000
--- a/test-suite/bugs/opened/3320.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Goal forall x : nat, True.
-  fix 1.
-  assumption.
-Fail Qed.
diff --git a/test-suite/bugs/opened/3424.v b/test-suite/bugs/opened/3424.v
new file mode 100644
index 00000000..d1c5bb68
--- /dev/null
+++ b/test-suite/bugs/opened/3424.v
@@ -0,0 +1,24 @@
+Set Universe Polymorphism.
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
+Class Contr_internal (A : Type) := BuildContr { center : A ; contr : (forall y : A, center = y) }.
+Inductive trunc_index : Type := minus_two | trunc_S (x : trunc_index).
+Bind Scope trunc_scope with trunc_index.
+Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
+  match n with
+    | minus_two => Contr_internal A
+    | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y)
+  end.
+Notation minus_one:=(trunc_S minus_two).
+Notation "0" := (trunc_S minus_one) : trunc_scope.
+Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A.
+Notation IsHProp := (IsTrunc minus_one).
+Notation IsHSet := (IsTrunc 0).
+Goal forall (A : Type) (a b : A) (H' : IsHSet A), { x : Type & IsHProp x }.
+Proof.
+intros.
+eexists.
+(* exact (H' a b). *)
+(* Undo. *)
+Fail apply (H' a b).
+exact (H' a b).
+Qed.
diff --git a/test-suite/bugs/opened/3794.v b/test-suite/bugs/opened/3794.v
index 99ca6cb3..e4711a38 100644
--- a/test-suite/bugs/opened/3794.v
+++ b/test-suite/bugs/opened/3794.v
@@ -4,4 +4,4 @@ Hint Unfold not : core.
 Goal true<>false.
 Set Typeclasses Debug.
 Fail typeclasses eauto with core.
-Abort.
-\ No newline at end of file
+Abort.
diff --git a/test-suite/bugs/opened/3916.v b/test-suite/bugs/opened/3916.v
deleted file mode 100644
index fd95503e..00000000
--- a/test-suite/bugs/opened/3916.v
+++ /dev/null
@@ -1,3 +0,0 @@
-Require Import List.
-
-Fail Hint Resolve -> in_map. (* Also happens when using <- instead of -> *)
diff --git a/test-suite/bugs/opened/3926.v b/test-suite/bugs/opened/3926.v
deleted file mode 100644
index cfad7635..00000000
--- a/test-suite/bugs/opened/3926.v
+++ /dev/null
@@ -1,30 +0,0 @@
-Notation compose := (fun g f x => g (f x)).
-Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope.
-Open Scope function_scope.
-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 ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with idpath => idpath end.
-Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A }.
-Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope.
-Local Open Scope equiv_scope.
-Axiom eisretr : forall {A B} (f : A -> B) `{IsEquiv A B f} x, f (f^-1 x) = x.
-Generalizable Variables A B C f g.
-Global Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g} : IsEquiv (compose g f) | 1000
-  := Build_IsEquiv A C (compose g f) (compose f^-1 g^-1).
-Definition isequiv_homotopic {A B} (f : A -> B) {g : A -> B} `{IsEquiv A B f} (h : forall x, f x = g x) : IsEquiv g
-  := Build_IsEquiv _ _ g (f ^-1).
-Global Instance isequiv_inverse {A B} (f : A -> B) `{IsEquiv A B f} : IsEquiv f^-1 | 10000
-  := Build_IsEquiv B A f^-1 f.
-Definition cancelR_isequiv {A B C} (f : A -> B) {g : B -> C}
-  `{IsEquiv A B f} `{IsEquiv A C (g o f)}
-  : IsEquiv g.
-Proof.
-  Unset Typeclasses Modulo Eta.
-  exact (isequiv_homotopic (compose (compose g f) f^-1)
-                           (fun b => ap g (eisretr f b))) || fail "too early".
-  Undo.
-  Set Typeclasses Modulo Eta.
-  Set Typeclasses Dependency Order.
-  Set Typeclasses Debug.
-  Fail exact (isequiv_homotopic (compose (compose g f) f^-1)
-                           (fun b => ap g (eisretr f b))).
diff --git a/test-suite/bugs/opened/3948.v b/test-suite/bugs/opened/3948.v
deleted file mode 100644
index 16581308..00000000
--- a/test-suite/bugs/opened/3948.v
+++ /dev/null
@@ -1,25 +0,0 @@
-Module Type S.
-Parameter t : Type.
-End S.
-
-Module Bar(X : S).
-Proof.
-  Definition elt := X.t.
-  Axiom fold : elt.
-End Bar.
-
-Module Make (X: S) := Bar(X).
-
-Declare Module X : S.
-
-Module Type Interface.
-  Parameter constant : unit.
-End Interface.
-
-Module DepMap : Interface.
-  Module Dom := Make(X).
-  Definition constant : unit :=
-    let _ := @Dom.fold in tt.
-End DepMap.
-
-Print Assumptions DepMap.constant.
-\ No newline at end of file
diff --git a/test-suite/bugs/opened/4717.v b/test-suite/bugs/opened/4717.v
deleted file mode 100644
index 9ad47467..00000000
--- a/test-suite/bugs/opened/4717.v
+++ /dev/null
@@ -1,19 +0,0 @@
-(*See below. They sometimes work, and sometimes do not. Is this a bug?*)
-
-Require Import Omega Psatz.
-
-Definition foo := nat.
-
-Goal forall (n : foo), 0 = n - n.
-Proof. intros. omega. (* works *) Qed.
-
-Goal forall (x n : foo), x = x + n - n.
-Proof.
-  intros.
-  Fail omega. (* Omega can't solve this system *)
-  Fail lia. (* Cannot find witness. *)
-  unfold foo in *.
-  omega. (* works *)
-Qed.
-
-(* Guillaume Melquiond: What matters is the equality. In the first case, it is @eq nat. In the second case, it is @eq foo. The same issue exists for ring and field. So it is not a bug, but it is worth fixing.*)
diff --git a/test-suite/bugs/opened/4803.v b/test-suite/bugs/opened/4803.v
deleted file mode 100644
index 4530548b..00000000
--- a/test-suite/bugs/opened/4803.v
+++ /dev/null
@@ -1,48 +0,0 @@
-(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
-(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5.  If they use*)
-Require Import Coq.Lists.List.
-Require Import Coq.Vectors.Vector.
-Import ListNotations.
-Import VectorNotations.
-Set Implicit Arguments.
-Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T).
-Arguments mynil {_}, _.
-
-Delimit Scope mylist_scope with mylist.
-Bind Scope mylist_scope with mylist.
-Delimit Scope vector_scope with vector.
-
-Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
-Notation " [ x ] " := (mycons x mynil) : mylist_scope.
-Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope.
-
-(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4.  There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *)
-Check [ ]%mylist : mylist _.
-Check [ ]%list : list _.
-Check []%vector : Vector.t _ _.
-Check [ _ ]%mylist : mylist _.
-Check [ _ ]%list : list _.
-Check [ _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%list : list _.
-Check [ _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
-
-(** Now check that we can add and then remove notations from the parser *)
-(* We should be able to stick some vernacular here to remove [] from the parser *)
-Fail Remove Notation "[]".
-Goal True.
-  (* This should not be a syntax error; before moving this file to closed, uncomment this line. *)
-  (* idtac; []. *)
-  constructor.
-Qed.
-
-Check { _ : _ & _ }.
-Reserved Infix "&" (at level 0).
-Fail Remove Infix "&".
-(* Check { _ : _ & _ }. *)
diff --git a/test-suite/bugs/opened/4813.v b/test-suite/bugs/opened/4813.v
index b7517017..2ac55359 100644
--- a/test-suite/bugs/opened/4813.v
+++ b/test-suite/bugs/opened/4813.v
@@ -1,5 +1,5 @@
-(* An example one would like to see succeeding *)
+Require Import Program.Tactics.
 
 Record T := BT { t : Set }.
 Record U (x : T) := BU { u : t x -> Prop }.
-Fail Definition A (H : unit -> Prop) : U (BT unit) := BU _ H.
+Program Definition A (H : unit -> Prop) : U (BT unit) := BU _ H.
diff --git a/test-suite/bugs/opened/6393.v b/test-suite/bugs/opened/6393.v
new file mode 100644
index 00000000..8d5d0923
--- /dev/null
+++ b/test-suite/bugs/opened/6393.v
@@ -0,0 +1,11 @@
+(* These always worked. *)
+Goal prod True True. firstorder. Qed.
+Goal True -> @sigT True (fun _ => True). firstorder. Qed.
+Goal prod True True. dtauto. Qed.
+Goal prod True True. tauto. Qed.
+
+(* These should work. *)
+Goal @sigT True (fun _ => True). dtauto. Qed.
+(* These should work, but don't *)
+(* Goal @sigT True (fun _ => True). firstorder. Qed. *)
+(* Goal @sigT True (fun _ => True). tauto. Qed. *)
diff --git a/test-suite/bugs/opened/6602.v b/test-suite/bugs/opened/6602.v
new file mode 100644
index 00000000..3690adf9
--- /dev/null
+++ b/test-suite/bugs/opened/6602.v
@@ -0,0 +1,17 @@
+Require Import Omega.
+
+Lemma test_nat:
+  forall n, (5 + pred n <= 5 + n).
+Proof.
+  intros.
+  zify.
+  omega.
+Qed.
+
+Lemma test_N:
+  forall n, (5 + N.pred n <= 5 + n)%N.
+Proof.
+  intros.
+  zify.
+  omega.
+Qed.