Update various polyproj bugs w.r.t. latest trunk

12 files changed, 9 insertions, 763 deletions

diff --git a/test-suite/bugs/opened/HoTT_coq_007.v b/test-suite/bugs/opened/HoTT_coq_007.v
index f609aff5d7..63e3220c55 100644
--- a/test-suite/bugs/opened/HoTT_coq_007.v
+++ b/test-suite/bugs/opened/HoTT_coq_007.v
@@ -36,14 +36,14 @@ Module Comment1.
   Set Printing All.
   Set Printing Universes.
 
-  Fail Lemma foo objC (C : @Category objC) (C0 : Category (Functor Cat0 C)) (x : Functor Cat0 Cat0) : forall (y : Functor C0 Cat0) z, (ComposeFunctors y z = x). (** ??? The term "y" has type
+  Lemma foo objC (C : @Category objC) (C0 : Category (Functor Cat0 C)) (x : Functor Cat0 Cat0) : forall (y : Functor C0 Cat0) z, (ComposeFunctors y z = x). (** ??? The term "y" has type
  "@Functor (* Top.448 Top.449 Top.450 Top.451 *)
     (@Functor (* Set Top.441 Top.442 Top.336 *) Empty_set Cat0 objC C) C0
     Empty_set Cat0" while it is expected to have type
  "@Functor (* Top.295 Top.296 Top.295 Top.296 *) ?46 ?47 ?48 ?49"
 (Universe inconsistency: Cannot enforce Set = Top.295)). *)
-  Fail intro. (* Illegal application (Type Error) *)
-  Fail Abort.
+    intro. (* Illegal application (Type Error) *)
+  Abort.
 End Comment1.
 
 Module Comment2.
diff --git a/test-suite/bugs/opened/HoTT_coq_027.v b/test-suite/bugs/opened/HoTT_coq_027.v
index 2f8ec87491..3a8a2cf0c4 100644
--- a/test-suite/bugs/opened/HoTT_coq_027.v
+++ b/test-suite/bugs/opened/HoTT_coq_027.v
@@ -20,10 +20,9 @@ Identity Coercion FunctorToType_Id : FunctorToType >-> Functor.
 
 Definition FunctorTo_Set2Type `(C : @Category objC) (F : FunctorToSet C)
 : FunctorToType C.
-  Fail refine (@Build_Functor _ C _ TypeCat
+  refine (@Build_Functor _ C _ TypeCat
                          (fun x => F.(ObjectOf) x)
                          (fun s d m => F.(MorphismOf) _ _ m)).
-  admit.
 Defined. (* Toplevel input, characters 0-8:
 Error:
 The term
@@ -50,10 +49,12 @@ Record SetGrothendieckPair `(C : @Category objC) (F' : Functor C SetCat) :=
 Section SetGrothendieckCoercion.
   Context `(C : @Category objC).
   Variable F : Functor C SetCat.
-  Let F' := (F : FunctorToSet _) : FunctorToType _.
+  Fail Let F' := (F : FunctorToSet _) : FunctorToType _. (* The command has indeed failed with message:
+=> Anomaly: apply_coercion_args: mismatch between arguments and coercion.
+Please report. *)
 
   Set Printing Universes.
-  Definition SetGrothendieck2Grothendieck (G : SetGrothendieckPair F) : GrothendieckPair F'
+  Fail Definition SetGrothendieck2Grothendieck (G : SetGrothendieckPair F) : GrothendieckPair F'
     := {| GrothendieckC := G.(SetGrothendieckC); GrothendieckX := G.(SetGrothendieckX) : F' _ |}.
   (* Toplevel input, characters 0-187:
 Error: Illegal application:
diff --git a/test-suite/bugs/opened/HoTT_coq_036.v b/test-suite/bugs/opened/HoTT_coq_036.v
deleted file mode 100644
index 3c480eea5f..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_036.v
+++ /dev/null
@@ -1,135 +0,0 @@
-Module Version1.
-  Set Implicit Arguments.
-  Set Universe Polymorphism.
-  Generalizable All Variables.
-
-  Record SpecializedCategory (obj : Type) :=
-    {
-      Object :> _ := obj
-    }.
-
-  Record > Category :=
-    {
-      CObject : Type;
-      UnderlyingCategory :> @SpecializedCategory CObject
-    }.
-
-  Record SpecializedFunctor `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) :=
-    {
-      ObjectOf :> objC -> objD
-    }.
-
-  Definition Functor (C D : Category) := SpecializedFunctor C D.
-
-  Parameter TerminalCategory : SpecializedCategory unit.
-
-  Definition focus A (_ : A) := True.
-
-  Definition CommaCategory_Object (A : Category) (S : Functor TerminalCategory A) : Type.
-    assert (Hf : focus ((S tt) = (S tt))) by constructor.
-    let C1 := constr:(CObject) in
-    let C2 := constr:(fun C => @Object (CObject C) C) in
-    unify C1 C2.
-    Fail progress change CObject with (fun C => @Object (CObject C) C) in *.
-    simpl in *.
-    match type of Hf with
-      | focus ?V => exact V
-    end.
-  Defined.
-
-  Definition Build_SliceCategory (A : Category) (F : Functor TerminalCategory A) := @Build_SpecializedCategory (CommaCategory_Object F).
-  Parameter SetCat : @SpecializedCategory Set.
-
-  Set Printing Universes.
-  Check (fun (A : Category) (F : Functor TerminalCategory A) => @Build_SpecializedCategory (CommaCategory_Object F)) SetCat.
-  (* (fun (A : Category (* Top.68 *))
-   (F : Functor (* Set Top.68 *) TerminalCategory A) =>
- {|  |}) SetCat (* Top.68 *)
-     : forall
-         F : Functor (* Set Top.68 *) TerminalCategory SetCat (* Top.68 *),
-       let Object := CommaCategory_Object (* Top.68 Top.69 Top.68 *) F in
-       SpecializedCategory (* Top.69 *)
-         (CommaCategory_Object (* Top.68 Top.69 Top.68 *) F) *)
-  Check @Build_SliceCategory SetCat. (* Toplevel input, characters 0-34:
-Error: Universe inconsistency (cannot enforce Top.51 <= Set because Set
-< Top.51). *)
-End Version1.
-
-Module Version2.
-  Set Implicit Arguments.
-  Set Universe Polymorphism.
-
-  Record SpecializedCategory (obj : Type) :=
-    {
-      Object : _ := obj
-    }.
-
-  Record > Category :=
-    {
-      CObject : Type;
-      UnderlyingCategory :> @SpecializedCategory CObject
-    }.
-
-  Parameter TerminalCategory : SpecializedCategory unit.
-
-  Definition focus A (_ : A) := True.
-  Parameter ObjectOf' : forall (objC : Type) (C : SpecializedCategory objC)
-                               (objD : Type) (D : SpecializedCategory objD), Prop.
-  Definition CommaCategory_Object (A : Category) : Type.
-    assert (Hf : focus (@ObjectOf' _ (@Build_Category unit TerminalCategory) _ A)) by constructor.
-    Fail progress change CObject with (fun C => @Object (CObject C) C) in *;
-      simpl in *.
-    match type of Hf with
-      | focus ?V => exact V
-    end.
-  Defined.
-
-  Definition Build_SliceCategory := @CommaCategory_Object.
-  Parameter SetCat : @SpecializedCategory Set.
-
-  Set Printing Universes.
-  Check @Build_SliceCategory SetCat.
-End Version2.
-
-Module OtherBug.
-  Set Implicit Arguments.
-  Set Universe Polymorphism.
-
-  Record SpecializedCategory (obj : Type) :=
-    {
-      Object : _ := obj
-    }.
-
-  Record > Category :=
-    {
-      CObject : Type;
-      UnderlyingCategory :> @SpecializedCategory CObject
-    }.
-
-  Parameter TerminalCategory : SpecializedCategory unit.
-
-  Definition focus A (_ : A) := True.
-
-  Parameter ObjectOf' : forall (objC : Type) (C : SpecializedCategory objC)
-                               (objD : Type) (D : SpecializedCategory objD), Prop.
-  Definition CommaCategory_Object (A : Category) : Type.
-    assert (Hf : focus (@ObjectOf' _ (@Build_Category unit TerminalCategory) _ A)) by constructor.
-    Fail progress change CObject with (fun C => @Object (CObject C) C) in *;
-      simpl in *.
-    match type of Hf with
-      | focus ?V => exact V
-    end.
-  Defined.
-
-  Parameter SetCat : @SpecializedCategory Set.
-
-  Set Printing Universes.
-  Definition Build_SliceCategory := @CommaCategory_Object.
-  Check @CommaCategory_Object SetCat.
-  (* CommaCategory_Object (* Top.43 Top.44 Top.43 *) SetCat (* Top.43 *)
-     : Type (* Top.44 *) *)
-  Check @Build_SliceCategory SetCat.
-  (* Toplevel input, characters 0-34:
-Error: Universe inconsistency (cannot enforce Top.36 <= Set because Set
-< Top.36). *)
-End OtherBug.
diff --git a/test-suite/bugs/opened/HoTT_coq_045.v b/test-suite/bugs/opened/HoTT_coq_045.v
deleted file mode 100644
index 27b28e593f..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_045.v
+++ /dev/null
@@ -1,53 +0,0 @@
-Set Implicit Arguments.
-Set Universe Polymorphism.
-Generalizable All Variables.
-
-Record SpecializedCategory (obj : Type) :=
-  {
-    Object :> _ := obj
-  }.
-
-Record > Category :=
-  {
-    CObject : Type;
-    UnderlyingCategory :> @SpecializedCategory CObject
-  }.
-
-Record SpecializedFunctor `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) :=
-  {
-    ObjectOf :> objC -> objD
-  }.
-
-Definition Functor (C D : Category) := SpecializedFunctor C D.
-
-Parameter TerminalCategory : SpecializedCategory unit.
-
-Definition focus A (_ : A) := True.
-
-Definition CommaCategory_Object (A : Category) (S : Functor TerminalCategory A) : Type.
-  assert (Hf : focus ((S tt) = (S tt))) by constructor.
-  let C1 := constr:(CObject) in
-  let C2 := constr:(fun C => @Object (CObject C) C) in
-  unify C1 C2.
-  Fail progress change CObject with (fun C => @Object (CObject C) C) in *.
-  simpl in *.
-  let V := match type of Hf with
-             | focus ?V => constr:(V)
-           end
-  in exact V.
-(* Toplevel input, characters 89-96:
-Error: Illegal application:
-The term "ObjectOf" of type
- "forall (objC : Set) (C : SpecializedCategory objC)
-    (objD : Type) (D : SpecializedCategory objD),
-  SpecializedFunctor C D -> objC -> objD"
-cannot be applied to the terms
- "Object TerminalCategory" : "Type"
- "TerminalCategory" : "SpecializedCategory unit"
- "Object A" : "Type"
- "UnderlyingCategory A" : "SpecializedCategory (CObject A)"
- "S" : "Functor TerminalCategory A"
- "tt" : "unit"
-The 1st term has type "Type" which should be coercible to
-"Set". *)
-Defined.
diff --git a/test-suite/bugs/opened/HoTT_coq_053.v b/test-suite/bugs/opened/HoTT_coq_053.v
deleted file mode 100644
index f47f9b5250..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_053.v
+++ /dev/null
@@ -1,50 +0,0 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
-Set Printing Universes.
-Set Implicit Arguments.
-Generalizable All Variables.
-Set Asymmetric Patterns.
-Set Universe Polymorphism.
-
-Inductive Unit : Type :=
-    tt : Unit.
-
-Inductive Bool : Type :=
-  | true : Bool
-  | false : Bool.
-
-Inductive paths {A : Type} (a : A) : A -> Type :=
-  idpath : paths a a.
-
-Record PreCategory :=
-  {
-    Object :> Type;
-    Morphism : Object -> Object -> Type
-  }.
-
-Definition DiscreteCategory X : PreCategory
-  := @Build_PreCategory X
-                        (@paths X).
-
-Definition IndiscreteCategory X : PreCategory
-  := @Build_PreCategory X
-                         (fun _ _ => Unit).
-
-Fail Definition NatCategory (n : nat) :=
-  match n with
-    | 0 => IndiscreteCategory Unit
-    | _ => DiscreteCategory Bool
-  end.
-(* Error: Universe inconsistency (cannot enforce Set <= Prop).*)
-
-Definition NatCategory' (n : nat) :=
-  match n with
-    | 0 => (fun X => @Build_PreCategory X
-                         (fun _ _ => Unit : Prop)) Unit
-    | _ => DiscreteCategory Bool
-  end.
-
-Fail Definition NatCategory'' (n : nat) :=
-  match n with
-    | 0 => IndiscreteCategory Unit
-    | _ => DiscreteCategory Bool
-  end.
diff --git a/test-suite/bugs/opened/HoTT_coq_054.v b/test-suite/bugs/opened/HoTT_coq_054.v
deleted file mode 100644
index fd37eb3300..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_054.v
+++ /dev/null
@@ -1,94 +0,0 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
-Inductive Empty : Prop := .
-
-Inductive paths {A : Type} (a : A) : A -> Type :=
-  idpath : paths a a.
-
-Notation "x = y :> A" := (@paths A x y) : type_scope.
-Notation "x = y" := (x = y :>_) : type_scope.
-
-Arguments idpath {A a} , [A] a.
-
-Definition idmap {A : Type} : A -> A := fun x => x.
-
-Definition path_sum {A B : Type} (z z' : A + B)
-           (pq : match z, z' with
-                   | inl z0, inl z'0 => z0 = z'0
-                   | inr z0, inr z'0 => z0 = z'0
-                   | _, _ => Empty
-                 end)
-: z = z'.
-  destruct z, z', pq; exact idpath.
-Defined.
-
-Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
-  := match p with idpath => idpath end.
-
-Fail Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B)
-              (* Fortunately, this unifies properly *)
-              (pq : match (x, y) with (inl x', inl y') => x' = y' | (inr x', inr y') => x' = y' | _ => Empty end) :
-  let f z := match z with inl z' => inl (g z') | inr z' => inr (h z') end in
-  ap f (path_sum x y pq) = path_sum (f x) (f y)
-     (* Coq appears to require *ALL* of the annotations *)
-     ((match x as x return match (x, y) with
-              (inl x', inl y') => x' = y'
-            | (inr x', inr y') => x' = y'
-            | _ => Empty
-          end -> match (f x, f y) with
-               | (inl x', inl y') => x' = y'
-               | (inr x', inr y') => x' = y'
-               | _ => Empty end with
-           | inl x' => match y as y return match y with
-                                               inl y' => x' = y'
-                                             | _ => Empty
-                                           end -> match f y with
-                                                    | inl y' => g x' = y'
-                                                    | _ => Empty end with
-                         | inl y' => ap g
-                         | inr y' => idmap
-                       end
-           | inr x' => match y as y return match y with
-                                               inr y' => x' = y'
-                                             | _ => Empty
-                                           end -> match f y with
-                                                    | inr y' => h x' = y'
-                                                    | _ => Empty end with
-                         | inl y' => idmap
-                         | inr y' => ap h
-                       end
-       end) pq).
-  Fail destruct x; destruct y; destruct pq; reflexivity.
-Fail Qed.
-(* Toplevel input, characters 1367-1374:
-Error:
-In environment
-A : Type
-B : Type
-A' : Type
-B' : Type
-g : A -> A'
-h : B -> B'
-x : A + B
-y : A + B
-pq :
-match x with
-| inl x' => match y with
-            | inl y' => x' = y'
-            | inr _ => Empty
-            end
-| inr x' => match y with
-            | inl _ => Empty
-            | inr y' => x' = y'
-            end
-end
-f :=
-fun z : A + B =>
-match z with
-| inl z' => inl (g z')
-| inr z' => inr (h z')
-end : A + B -> A' + B'
-x' : B
-y0 : A + B
-y' : B
-The term "x' = y'" has type "Type" while it is expected to have type
-"Prop" (Universe inconsistency). *)
diff --git a/test-suite/bugs/opened/HoTT_coq_062.v b/test-suite/bugs/opened/HoTT_coq_062.v
index 99c2a1fb58..ce35818efd 100644
--- a/test-suite/bugs/opened/HoTT_coq_062.v
+++ b/test-suite/bugs/opened/HoTT_coq_062.v
@@ -70,7 +70,7 @@ Theorem thm `{Univalence} : (forall A, ((A -> False) -> False) -> A) -> False.
   intro f.
   Set Printing Universes.
   Set Printing All.
-  Fail pose proof (apD f (path_universe e)).
+  pose proof (apD f (path_universe e)).
   Fail pose proof (apD f p).
 (* Toplevel input, characters 18-19:
 Error:
diff --git a/test-suite/bugs/opened/HoTT_coq_064.v b/test-suite/bugs/opened/HoTT_coq_064.v
deleted file mode 100644
index 98e815aefc..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_064.v
+++ /dev/null
@@ -1,187 +0,0 @@
-(* File reduced by coq-bug-finder from 279 lines to 219 lines. *)
-
-Set Implicit Arguments.
-Set Universe Polymorphism.
-Definition admit {T} : T.
-Admitted.
-Module Export Overture.
-  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 :> A" := (@paths A x y) : type_scope.
-
-  Notation "x = y" := (x = y :>_) : type_scope.
-
-  Delimit Scope path_scope with path.
-
-  Local Open Scope path_scope.
-
-  Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
-    := match p with idpath => idpath end.
-
-  Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
-  : forall x, f x = g x
-    := fun x => match h with idpath => idpath end.
-
-  Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { equiv_inv : B -> A }.
-
-  Delimit Scope equiv_scope with equiv.
-  Local Open Scope equiv_scope.
-
-  Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : equiv_scope.
-
-  Class Funext :=
-    { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
-
-  Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x) :
-    (forall x, f x = g x) -> f = g
-    :=
-      (@apD10 A P f g)^-1.
-
-End Overture.
-
-Module Export Core.
-
-  Set Implicit Arguments.
-  Delimit Scope morphism_scope with morphism.
-  Delimit Scope category_scope with category.
-  Delimit Scope object_scope with object.
-
-  Record PreCategory :=
-    {
-      object :> Type;
-      morphism : object -> object -> Type;
-
-      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)
-    }.
-  Bind Scope category_scope with PreCategory.
-  Arguments compose [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename.
-
-  Infix "o" := compose : morphism_scope.
-
-End Core.
-
-Local Open Scope morphism_scope.
-Record Functor (C D : PreCategory) :=
-  {
-    object_of :> C -> D;
-    morphism_of : forall s d, morphism C s d
-                              -> morphism D (object_of s) (object_of d)
-  }.
-
-Inductive Unit : Set :=
-  tt : Unit.
-
-Definition indiscrete_category (X : Type) : PreCategory
-  := @Build_PreCategory X
-                        (fun _ _ => Unit)
-                        (fun _ _ _ _ _ => tt)
-                        (fun _ _ _ _ _ _ _ => idpath).
-
-
-Record NaturalTransformation C D (F G : Functor C D) := { components_of :> forall c, morphism D (F c) (G c) }.
-Section path_natural_transformation.
-  Context `{Funext}.
-  Variable C : PreCategory.
-  Variable D : PreCategory.
-  Variables F G : Functor C D.
-
-  Section path.
-    Variables T U : NaturalTransformation F G.
-    Lemma path'_natural_transformation
-    : components_of T = components_of U
-      -> T = U.
-      admit.
-    Defined.
-    Lemma path_natural_transformation
-    : (forall x, T x = U x)
-      -> T = U.
-    Proof.
-      intros.
-      apply path'_natural_transformation.
-      apply path_forall; assumption.
-    Qed.
-  End path.
-End path_natural_transformation.
-Ltac path_natural_transformation :=
-  repeat match goal with
-           | _ => intro
-           | _ => apply path_natural_transformation; simpl
-         end.
-Definition comma_category A B C (S : Functor A C) (T : Functor B C)
-: PreCategory.
-  admit.
-Defined.
-Definition compose C D (F F' F'' : Functor C D)
-           (T' : NaturalTransformation F' F'') (T : NaturalTransformation F F')
-: NaturalTransformation F F''
-  := Build_NaturalTransformation F F''
-                                 (fun c => T' c o T c).
-
-Infix "o" := compose : natural_transformation_scope.
-
-Local Open Scope natural_transformation_scope.
-
-Definition associativity `{fs : Funext}
-           C D F G H I
-           (V : @NaturalTransformation C D F G)
-           (U : @NaturalTransformation C D G H)
-           (T : @NaturalTransformation C D H I)
-: (T o U) o V = T o (U o V).
-Proof.
-  path_natural_transformation.
-
-  apply associativity.
-Qed.
-Definition functor_category `{Funext} (C D : PreCategory) : PreCategory
-  := @Build_PreCategory (Functor C D)
-                        (@NaturalTransformation C D)
-                        (@compose C D)
-                        (@associativity _ C D).
-
-Notation "C -> D" := (functor_category C D) : category_scope.
-
-Definition compose_functor `{Funext} (C D E : PreCategory) : object ((C -> D) -> ((D -> E) -> (C -> E))).
-  admit.
-
-Defined.
-
-Definition pullback_along `{Funext} (C C' D : PreCategory) (p : Functor C C')
-: object ((C' -> D) -> (C -> D))
-  := Eval hnf in compose_functor _ _ _ p.
-
-Definition IsColimit `{Funext} C D (F : Functor D C) (x : object
-                                                            (@comma_category (indiscrete_category Unit)
-                                                                             (@functor_category H (indiscrete_category Unit) C)
-                                                                             (@functor_category H D C)
-                                                                             admit
-                                                                             (@pullback_along H D (indiscrete_category Unit) C
-                                                                                              admit))) : Type
-  := admit.
-
-Generalizable All Variables.
-Axiom fs : Funext.
-
-Section bar.
-
-  Variable D : PreCategory.
-
-  Fail Context `(has_colimits
-            : forall F : Functor D C,
-                @IsColimit _ C D F (colimits F)).
-(* Error: Unsatisfied constraints: Top.3773 <= Set
- (maybe a bugged tactic). *)
diff --git a/test-suite/bugs/opened/HoTT_coq_098.v b/test-suite/bugs/opened/HoTT_coq_098.v
deleted file mode 100644
index a07f2f0fa2..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_098.v
+++ /dev/null
@@ -1,84 +0,0 @@
-Set Implicit Arguments.
-Generalizable All Variables.
-
-Polymorphic Record SpecializedCategory (obj : Type) := Build_SpecializedCategory' {
-  Object :> _ := obj;
-  Morphism' : obj -> obj -> Type;
-
-  Identity' : forall o, Morphism' o o;
-  Compose' : forall s d d', Morphism' d d' -> Morphism' s d -> Morphism' s d'
-}.
-
-Polymorphic Definition TypeCat : @SpecializedCategory Type
-  := (@Build_SpecializedCategory' Type
-                                  (fun s d => s -> d)
-                                  (fun _ => (fun x => x))
-                                  (fun _ _ _ f g => (fun x => f (g x)))).
-
-Inductive GraphIndex := GraphIndexSource | GraphIndexTarget.
-Polymorphic Definition GraphIndexingCategory : @SpecializedCategory GraphIndex.
-Admitted.
-
-Module success.
-  Section SpecializedFunctor.
-    Set Universe Polymorphism.
-    Context `(C : @SpecializedCategory objC).
-    Context `(D : @SpecializedCategory objD).
-    Unset Universe Polymorphism.
-
-    Polymorphic Record SpecializedFunctor
-      := {
-          ObjectOf' : objC -> objD;
-          MorphismOf' : forall s d, C.(Morphism') s d -> D.(Morphism') (ObjectOf' s) (ObjectOf' d)
-        }.
-  End SpecializedFunctor.
-
-  Polymorphic Definition UnderlyingGraph : SpecializedFunctor GraphIndexingCategory TypeCat.
-  Admitted.
-End success.
-
-Module failure.
-  Section SpecializedFunctor.
-    Context `(C : @SpecializedCategory objC).
-    Context `(D : @SpecializedCategory objD).
-
-    Polymorphic Record SpecializedFunctor
-      := {
-          ObjectOf' : objC -> objD;
-          MorphismOf' : forall s d, C.(Morphism') s d -> D.(Morphism') (ObjectOf' s) (ObjectOf' d)
-        }.
-  End SpecializedFunctor.
-
-  Set Printing Universes.
-  Fail Polymorphic Definition UnderlyingGraph : SpecializedFunctor GraphIndexingCategory TypeCat.
-  (* Toplevel input, characters 73-94:
-Error:
-The term "GraphIndexingCategory (* Top.563 *)" has type
- "SpecializedCategory (* Top.563 Set *) GraphIndex"
-while it is expected to have type
- "SpecializedCategory (* Top.550 Top.551 *) ?7"
-(Universe inconsistency: Cannot enforce Set = Top.551)). *)
-End failure.
-
-Module polycontext.
-  Section SpecializedFunctor.
-    Context `(C : @SpecializedCategory objC).
-    Context `(D : @SpecializedCategory objD).
-
-    Polymorphic Record SpecializedFunctor
-      := {
-          ObjectOf' : objC -> objD;
-          MorphismOf' : forall s d, C.(Morphism') s d -> D.(Morphism') (ObjectOf' s) (ObjectOf' d)
-        }.
-  End SpecializedFunctor.
-
-  Set Printing Universes.
-  Fail Polymorphic Definition UnderlyingGraph : SpecializedFunctor GraphIndexingCategory TypeCat.
-  (* Toplevel input, characters 73-94:
-Error:
-The term "GraphIndexingCategory (* Top.563 *)" has type
- "SpecializedCategory (* Top.563 Set *) GraphIndex"
-while it is expected to have type
- "SpecializedCategory (* Top.550 Top.551 *) ?7"
-(Universe inconsistency: Cannot enforce Set = Top.551)). *)
-End polycontext.
diff --git a/test-suite/bugs/opened/HoTT_coq_102.v b/test-suite/bugs/opened/HoTT_coq_102.v
deleted file mode 100644
index 9d87517e1c..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_102.v
+++ /dev/null
@@ -1,27 +0,0 @@
-(* File reduced by coq-bug-finder from 64 lines to 30 lines. *)
-Set Implicit Arguments.
-Set Universe Polymorphism.
-Generalizable All Variables.
-Record SpecializedCategory (obj : Type) := { Object :> _ := obj }.
-
-Record > Category :=
-  { CObject : Type;
-    UnderlyingCategory :> @SpecializedCategory CObject }.
-
-Record SpecializedFunctor `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) :=
-  { ObjectOf :> objC -> objD }.
-
-Definition Functor (C D : Category) := SpecializedFunctor C D.
-
-Parameter TerminalCategory : SpecializedCategory unit.
-
-Definition focus A (_ : A) := True.
-
-Definition CommaCategory_Object (A : Category) (S : Functor TerminalCategory A) : Type.
-  assert (Hf : focus ((S tt) = (S tt))) by constructor.
-  let C1 := constr:(CObject) in
-  let C2 := constr:(fun C => @Object (CObject C) C) in
-  let check := constr:(eq_refl : C1 = C2) in
-  unify C1 C2.
-  Fail progress change CObject with (fun C => @Object (CObject C) C) in *.
-  (* not convertible *)
diff --git a/test-suite/bugs/opened/HoTT_coq_107.v b/test-suite/bugs/opened/HoTT_coq_107.v
deleted file mode 100644
index f8b595d859..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_107.v
+++ /dev/null
@@ -1,106 +0,0 @@
-(* -*- mode: coq; coq-prog-args: ("-nois" "-emacs") -*- *)
-(* File reduced by coq-bug-finder from 4897 lines to 2605 lines, then from 2297 lines to 236 lines, then from 239 lines to 137 lines, then from 118 lines to 67 lines, then from 520 lines to 76 lines. *)
-(** Note: The bug here is the same as the #113, that is, HoTT_coq_113.v *)
-Require Import Coq.Init.Logic.
-Global Set Universe Polymorphism.
-Global Set Asymmetric Patterns.
-Set Implicit Arguments.
-
-Inductive sigT (A:Type) (P:A -> Type) : Type :=
-  existT : forall x:A, P x -> sigT P.
-
-Notation "{ x : A  & P }" := (sigT (fun x:A => P)) : type_scope.
-
-Generalizable All Variables.
-Definition admit {T} : T.
-Admitted.
-Inductive paths {A : Type} (a : A) : A -> Type :=
-  idpath : paths a a.
-
-Notation "x = y :> A" := (@paths A x y) : type_scope.
-Notation "x = y" := (x = y :>_) : type_scope.
-Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
-  match p with idpath => u end.
-Class Contr_internal (A : Type) :=
-  BuildContr {
-      center : A ;
-      contr : (forall y : A, center = y)
-    }.
-
-Arguments center A {_}.
-
-Inductive trunc_index : Type :=
-| minus_two : trunc_index
-| trunc_S : trunc_index -> 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.
-
-Class IsTrunc (n : trunc_index) (A : Type) : Type :=
-  Trunc_is_trunc : IsTrunc_internal n A.
-
-Notation Contr := (IsTrunc minus_two).
-
-Hint Extern 0 => progress change Contr_internal with Contr in * : typeclass_instances.
-
-Definition path_contr `{Contr A} (x y : A) : x = y
-  := admit.
-
-Definition path_sigma' {A : Type} (P : A -> Type) {x x' : A} {y : P x} {y' : P x'}
-           (p : x = x') (q : transport _ p y = y')
-: existT _ x y = existT _ x' y'
-  := admit.
-Instance trunc_sigma `{P : A -> Type}
-         `{IsTrunc n A} `{forall a, IsTrunc n (P a)}
-: IsTrunc n (sigT P) | 100.
-
-Proof.
-  generalize dependent A.
-  induction n; [ | admit ]; simpl; intros A P ac Pc.
-  (exists (existT _ (center A) (center (P (center A))))).
-  intros [a ?].
-  refine (path_sigma' P (contr a) (path_contr _ _)).
-Defined.
-Inductive Bool : Set := true | false.
-Definition trunc_sum' n A B `{IsTrunc n Bool, IsTrunc n A, IsTrunc n B}
-: (IsTrunc n { b : Bool & if b then A else B }).
-Proof.
-  Set Printing All.
-  Set Printing Universes.
-  Fail refine (@trunc_sigma Bool (fun b => if b then A else B) n _ _).
-  (* Toplevel input, characters 23-76:
-Error:
-In environment
-n : trunc_index
-A : Type (* Top.193 *)
-B : Type (* Top.194 *)
-H : IsTrunc (* Set *) n Bool
-H0 : IsTrunc (* Top.193 *) n A
-H1 : IsTrunc (* Top.194 *) n B
-The term
- "@trunc_sigma (* Top.198 Top.199 Top.200 Top.201 *) Bool
-    (fun b : Bool =>
-     match b return Type (* Top.199 *) with
-     | true => A
-     | false => B
-     end) n ?49 ?50" has type
- "IsTrunc (* Top.200 *) n
-    (@sig (* Top.199 Top.199 *) Bool
-       (fun b : Bool =>
-        match b return Type (* Top.199 *) with
-        | true => A
-        | false => B
-        end))" while it is expected to have type
- "IsTrunc (* Top.195 *) n
-    (@sig (* Set Top.197 *) Bool
-       (fun b : Bool =>
-        match b return Type (* Top.197 *) with
-        | true => A
-        | false => B
-        end))" (Universe inconsistency: Cannot enforce Top.197 = Set)).
- *)
-  admit.
-Defined.
diff --git a/test-suite/bugs/opened/HoTT_coq_113.v b/test-suite/bugs/opened/HoTT_coq_113.v
deleted file mode 100644
index ae489e5f5b..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_113.v
+++ /dev/null
@@ -1,19 +0,0 @@
-(* File reduced by coq-bug-finder from original input, then from 3329 lines to 153 lines, then from 118 lines to 49 lines, then from 55 lines to 38 lines, then from 46 lines to 16 lines *)
-
-Generalizable All Variables.
-Set Universe Polymorphism.
-Class Foo (A : Type) := {}.
-Definition Baz := Foo.
-Definition Bar {A B} `{Foo A, Foo B} : True.
-Proof.
-  Set Printing Universes.
-  (* [change] should give fresh universes for each [Foo] *)
-  change Foo with Baz in *.
-  admit.
-Defined.
-Definition foo := @Bar nat.
-Fail Check @foo Set.
-(* Toplevel input, characters 26-29:
-Error:
-The term "Set" has type "Type (* Set+1 *)" while it is expected to have type
- "Set" (Universe inconsistency: Cannot enforce Set < Set because Set = Set)). *)