- Add an option to refresh only algebraic universes, for e_type_of. The goal

there is not the same as in Evd.define.
- Fixed bugs #3330 and #3331.

2 files changed, 0 insertions, 1119 deletions

diff --git a/test-suite/bugs/opened/3330.v b/test-suite/bugs/opened/3330.v
deleted file mode 100644
index face3b2d5..000000000
--- a/test-suite/bugs/opened/3330.v
+++ /dev/null
@@ -1,1083 +0,0 @@
-(* File reduced by coq-bug-finder from original input, then from 12106 lines to 1070 lines *)
-Module Export HoTT_DOT_Overture.
-Module Export HoTT.
-Module Export Overture.
-
-Definition relation (A : Type) := A -> A -> Type.
-Class Symmetric {A} (R : relation A) :=
-  symmetry : forall x y, R x y -> R y x.
-
-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.
-
-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 concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
-  match p, q with idpath, idpath => idpath end.
-
-Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
-  := match p with idpath => idpath end.
-
-Instance symmetric_paths {A} : Symmetric (@paths A) | 0 := @inverse A.
-
-Notation "1" := idpath : path_scope.
-
-Notation "p @ q" := (concat p q) (at level 20) : path_scope.
-
-Notation "p ^" := (inverse p) (at level 3) : path_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.
-
-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 pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x) : Type
-  := forall x:A, f x = g x.
-
-Hint Unfold pointwise_paths : typeclass_instances.
-
-Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope.
-
-Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
-  : f == g
-  := fun x => match h with idpath => 1 end.
-
-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) := BuildIsEquiv {
-  equiv_inv : B -> A ;
-  eisretr : Sect equiv_inv f;
-  eissect : Sect f equiv_inv;
-  eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
-}.
-
-Delimit Scope equiv_scope with equiv.
-
-Local Open Scope equiv_scope.
-
-Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : equiv_scope.
-
-Class Contr_internal (A : Type) := BuildContr {
-  center : A ;
-  contr : (forall y : A, center = y)
-}.
-
-Inductive trunc_index : Type :=
-| minus_two : trunc_index
-| trunc_S : trunc_index -> trunc_index.
-
-Fixpoint nat_to_trunc_index (n : nat) : trunc_index
-  := match n with
-       | 0 => trunc_S (trunc_S minus_two)
-       | S n' => trunc_S (nat_to_trunc_index n')
-     end.
-
-Coercion nat_to_trunc_index : nat >-> 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 IsHSet := (IsTrunc 0).
-
-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) :
-  f == g -> f = g
-  :=
-  (@apD10 A P f g)^-1.
-
-End Overture.
-
-End HoTT.
-
-End HoTT_DOT_Overture.
-
-Module Export HoTT_DOT_categories_DOT_Category_DOT_Core.
-
-Module Export HoTT.
-Module Export categories.
-Module Export Category.
-Module Export Core.
-Set Universe Polymorphism.
-
-Set Implicit Arguments.
-Delimit Scope morphism_scope with morphism.
-
-Delimit Scope category_scope with category.
-Delimit Scope object_scope with object.
-
-Record PreCategory :=
-  Build_PreCategory' {
-      object :> Type;
-      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;
-
-      trunc_morphism : forall s d, IsHSet (morphism s d)
-    }.
-
-Bind Scope category_scope with PreCategory.
-
-Arguments identity [!C%category] x%object : rename.
-Arguments compose [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename.
-
-Definition Build_PreCategory
-           object morphism compose identity
-           associativity left_identity right_identity
-  := @Build_PreCategory'
-       object
-       morphism
-       compose
-       identity
-       associativity
-       (fun _ _ _ _ _ _ _ => symmetry _ _ (associativity _ _ _ _ _ _ _))
-       left_identity
-       right_identity
-       (fun _ => left_identity _ _ _).
-
-Existing Instance trunc_morphism.
-
-Hint Resolve @left_identity @right_identity @associativity : category morphism.
-
-Module Export CategoryCoreNotations.
-
-  Infix "o" := compose : morphism_scope.
-End CategoryCoreNotations.
-End Core.
-
-End Category.
-
-End categories.
-
-End HoTT.
-
-End HoTT_DOT_categories_DOT_Category_DOT_Core.
-
-Module Export HoTT_DOT_types_DOT_Forall.
-
-Module Export HoTT.
-Module Export types.
-Module Export Forall.
-Generalizable Variables A B f g e n.
-
-Section AssumeFunext.
-
-Global Instance trunc_forall `{P : A -> Type} `{forall a, IsTrunc n (P a)}
-  : IsTrunc n (forall a, P a) | 100.
-
-admit.
-Defined.
-End AssumeFunext.
-
-End Forall.
-
-End types.
-
-End HoTT.
-
-End HoTT_DOT_types_DOT_Forall.
-
-Module Export HoTT_DOT_types_DOT_Prod.
-
-Module Export HoTT.
-Module Export types.
-Module Export Prod.
-Local Open Scope path_scope.
-
-Definition path_prod_uncurried {A B : Type} (z z' : A * B)
-  (pq : (fst z = fst z') * (snd z = snd z'))
-  : (z = z')
-  := match pq with (p,q) =>
-       match z, z' return
-         (fst z = fst z') -> (snd z = snd z') -> (z = z') with
-         | (a,b), (a',b') => fun p q =>
-           match p, q with
-             idpath, idpath => 1
-           end
-       end p q
-     end.
-
-Definition path_prod {A B : Type} (z z' : A * B) :
-  (fst z = fst z') -> (snd z = snd z') -> (z = z')
-  := fun p q => path_prod_uncurried z z' (p,q).
-
-Definition path_prod' {A B : Type} {x x' : A} {y y' : B}
-  : (x = x') -> (y = y') -> ((x,y) = (x',y'))
-  := fun p q => path_prod (x,y) (x',y') p q.
-
-End Prod.
-
-End types.
-
-End HoTT.
-
-End HoTT_DOT_types_DOT_Prod.
-
-Module Export HoTT_DOT_categories_DOT_Functor_DOT_Core.
-
-Module Export HoTT.
-Module Export categories.
-Module Export Functor.
-Module Export Core.
-Set Universe Polymorphism.
-
-Set Implicit Arguments.
-Delimit Scope functor_scope with functor.
-
-Local Open Scope morphism_scope.
-
-Section Functor.
-
-  Variable C : PreCategory.
-  Variable D : PreCategory.
-
-  Record Functor :=
-    {
-      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)
-    }.
-
-End Functor.
-Bind Scope functor_scope with Functor.
-
-Arguments morphism_of [C%category] [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch.
-Module Export FunctorCoreNotations.
-
-  Notation "F '_1' m" := (morphism_of F m) (at level 10, no associativity) : morphism_scope.
-End FunctorCoreNotations.
-End Core.
-
-End Functor.
-
-End categories.
-
-End HoTT.
-
-End HoTT_DOT_categories_DOT_Functor_DOT_Core.
-
-Module Export HoTT_DOT_categories_DOT_Category_DOT_Morphisms.
-
-Module Export HoTT.
-Module Export categories.
-Module Export Category.
-Module Export Morphisms.
-Set Universe Polymorphism.
-
-Local Open Scope morphism_scope.
-
-Class IsIsomorphism {C : PreCategory} {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 _
-  }.
-
-Class Isomorphic {C : PreCategory} s d :=
-  {
-    morphism_isomorphic :> morphism C s d;
-    isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic
-  }.
-
-Module Export CategoryMorphismsNotations.
-
-  Infix "<~=~>" := Isomorphic (at level 70, no associativity) : category_scope.
-
-End CategoryMorphismsNotations.
-End Morphisms.
-
-End Category.
-
-End categories.
-
-End HoTT.
-
-End HoTT_DOT_categories_DOT_Category_DOT_Morphisms.
-
-Module Export HoTT_DOT_categories_DOT_Category_DOT_Dual.
-
-Module Export HoTT.
-Module Export categories.
-Module Export Category.
-Module Export Dual.
-Set Universe Polymorphism.
-
-Local Open Scope morphism_scope.
-
-Section opposite.
-
-  Definition opposite (C : PreCategory) : 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)
-         _.
-End opposite.
-
-Module Export CategoryDualNotations.
-
-  Notation "C ^op" := (opposite C) (at level 3) : category_scope.
-End CategoryDualNotations.
-End Dual.
-
-End Category.
-
-End categories.
-
-End HoTT.
-
-End HoTT_DOT_categories_DOT_Category_DOT_Dual.
-
-Module Export HoTT_DOT_categories_DOT_Functor_DOT_Composition_DOT_Core.
-
-Module Export HoTT.
-Module Export categories.
-Module Export Functor.
-Module Export Composition.
-Module Export Core.
-Set Universe Polymorphism.
-
-Set Implicit Arguments.
-Local Open Scope morphism_scope.
-
-Section composition.
-
-  Variable C : PreCategory.
-  Variable D : PreCategory.
-  Variable E : PreCategory.
-  Variable G : Functor D E.
-  Variable F : Functor C D.
-
-  Local Notation c_object_of c := (G (F c)) (only parsing).
-
-  Local Notation c_morphism_of m := (morphism_of G (morphism_of F m)) (only parsing).
-
-  Let compose_composition_of' s d d'
-      (m1 : morphism C s d) (m2 : morphism C d d')
-  : c_morphism_of (m2 o m1) = c_morphism_of m2 o c_morphism_of m1.
-admit.
-Defined.
-  Definition compose_composition_of s d d' m1 m2
-    := Eval cbv beta iota zeta delta
-            [compose_composition_of'] in
-        @compose_composition_of' s d d' m1 m2.
-  Let compose_identity_of' x
-  : c_morphism_of (identity x) = identity (c_object_of x).
-
-admit.
-Defined.
-  Definition compose_identity_of x
-    := Eval cbv beta iota zeta delta
-            [compose_identity_of'] in
-        @compose_identity_of' x.
-  Definition compose : Functor C E
-    := Build_Functor
-         C E
-         (fun c => G (F c))
-         (fun _ _ m => morphism_of G (morphism_of F m))
-         compose_composition_of
-         compose_identity_of.
-
-End composition.
-Module Export FunctorCompositionCoreNotations.
-
-  Infix "o" := compose : functor_scope.
-End FunctorCompositionCoreNotations.
-End Core.
-
-End Composition.
-
-End Functor.
-
-End categories.
-
-End HoTT.
-
-End HoTT_DOT_categories_DOT_Functor_DOT_Composition_DOT_Core.
-
-Module Export HoTT_DOT_categories_DOT_Functor_DOT_Dual.
-
-Module Export HoTT.
-Module Export categories.
-Module Export Functor.
-Module Export Dual.
-Set Universe Polymorphism.
-
-Set Implicit Arguments.
-
-Section opposite.
-
-  Variable C : PreCategory.
-  Variable D : PreCategory.
-  Definition opposite (F : Functor C 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).
-
-End opposite.
-Module Export FunctorDualNotations.
-
-  Notation "F ^op" := (opposite F) : functor_scope.
-End FunctorDualNotations.
-End Dual.
-
-End Functor.
-
-End categories.
-
-End HoTT.
-
-End HoTT_DOT_categories_DOT_Functor_DOT_Dual.
-
-Module Export HoTT_DOT_categories_DOT_Functor_DOT_Identity.
-
-Module Export HoTT.
-Module Export categories.
-Module Export Functor.
-Module Export Identity.
-Set Universe Polymorphism.
-
-Section identity.
-
-  Definition identity C : Functor C C
-    := Build_Functor C C
-                     (fun x => x)
-                     (fun _ _ x => x)
-                     (fun _ _ _ _ _ => idpath)
-                     (fun _ => idpath).
-End identity.
-Module Export FunctorIdentityNotations.
-
-  Notation "1" := (identity _) : functor_scope.
-End FunctorIdentityNotations.
-End Identity.
-
-End Functor.
-
-End categories.
-
-End HoTT.
-
-End HoTT_DOT_categories_DOT_Functor_DOT_Identity.
-
-Module Export HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Core.
-
-Module Export HoTT.
-Module Export categories.
-Module Export NaturalTransformation.
-Module Export Core.
-Set Universe Polymorphism.
-
-Set Implicit Arguments.
-Local Open Scope morphism_scope.
-
-Section NaturalTransformation.
-
-  Variable C : PreCategory.
-  Variable D : PreCategory.
-  Variables F G : Functor C D.
-
-  Record NaturalTransformation :=
-    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
-      }.
-
-End NaturalTransformation.
-End Core.
-
-End NaturalTransformation.
-
-End categories.
-
-End HoTT.
-
-End HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Core.
-
-Module Export HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Dual.
-
-Module Export HoTT.
-Module Export categories.
-Module Export NaturalTransformation.
-Module Export Dual.
-Set Universe Polymorphism.
-
-Section opposite.
-
-  Variable C : PreCategory.
-  Variable D : PreCategory.
-
-  Definition opposite
-             (F G : Functor C D)
-             (T : NaturalTransformation F G)
-  : NaturalTransformation G^op F^op
-    := Build_NaturalTransformation' (G^op) (F^op)
-                                    (components_of T)
-                                    (fun s d => commutes_sym T d s)
-                                    (fun s d => commutes T d s).
-
-End opposite.
-
-End Dual.
-
-End NaturalTransformation.
-
-End categories.
-
-End HoTT.
-
-End HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Dual.
-
-Module Export HoTT_DOT_categories_DOT_Category_DOT_Strict.
-
-Module Export HoTT.
-Module Export categories.
-Module Export Category.
-Module Export Strict.
-
-Export Category.Core.
-Set Universe Polymorphism.
-
-End Strict.
-
-End Category.
-
-End categories.
-
-End HoTT.
-
-End HoTT_DOT_categories_DOT_Category_DOT_Strict.
-
-Module Export HoTT.
-Module Export categories.
-Module Export Category.
-Module Export Prod.
-Set Universe Polymorphism.
-
-Local Open Scope morphism_scope.
-
-Section prod.
-
-  Variable C : PreCategory.
-  Variable D : PreCategory.
-  Definition prod : PreCategory.
-
-    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.
-End prod.
-Module Export CategoryProdNotations.
-
-  Infix "*" := prod : category_scope.
-End CategoryProdNotations.
-End Prod.
-
-End Category.
-
-End categories.
-
-End HoTT.
-
-Module Functor.
-Module Export Prod.
-Set Universe Polymorphism.
-
-Set Implicit Arguments.
-Local Open Scope morphism_scope.
-
-Section proj.
-
-  Context {C : PreCategory}.
-  Context {D : PreCategory}.
-  Definition fst : Functor (C * D) C
-    := Build_Functor (C * D) C
-                     (@fst _ _)
-                     (fun _ _ => @fst _ _)
-                     (fun _ _ _ _ _ => idpath)
-                     (fun _ => idpath).
-
-  Definition snd : Functor (C * D) D
-    := Build_Functor (C * D) D
-                     (@snd _ _)
-                     (fun _ _ => @snd _ _)
-                     (fun _ _ _ _ _ => idpath)
-                     (fun _ => idpath).
-
-End proj.
-
-Section prod.
-
-  Variable C : PreCategory.
-  Variable D : PreCategory.
-  Variable D' : PreCategory.
-  Definition prod (F : Functor C D) (F' : Functor C 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))
-         (fun _ _ _ _ _ => path_prod' (composition_of F _ _ _ _ _)
-                                      (composition_of F' _ _ _ _ _))
-         (fun _ => path_prod' (identity_of F _) (identity_of F' _)).
-
-End prod.
-Local Infix "*" := prod : functor_scope.
-
-Section pair.
-
-  Variable C : PreCategory.
-  Variable D : PreCategory.
-  Variable C' : PreCategory.
-  Variable D' : PreCategory.
-  Variable F : Functor C D.
-  Variable F' : Functor C' D'.
-  Definition pair : Functor (C * C') (D * D')
-    := (F o fst) * (F' o snd).
-
-End pair.
-
-Module Export FunctorProdNotations.
-
-  Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : functor_scope.
-End FunctorProdNotations.
-End Prod.
-
-End Functor.
-
-Module Export HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Composition_DOT_Core.
-
-Module Export HoTT.
-Module categories.
-Module Export NaturalTransformation.
-Module Export Composition.
-Module Export Core.
-Set Universe Polymorphism.
-
-Set Implicit Arguments.
-Local Open Scope path_scope.
-
-Local Open Scope morphism_scope.
-
-Section composition.
-
-  Section compose.
-    Variable C : PreCategory.
-    Variable D : PreCategory.
-    Variables F F' F'' : Functor C D.
-    Variable T' : NaturalTransformation F' F''.
-
-    Variable T : NaturalTransformation F F'.
-    Local Notation CO c := (T' c o T c).
-
-    Definition compose_commutes s d (m : morphism C s d)
-    : CO d o morphism_of F m = morphism_of F'' m o CO s
-      := (associativity _ _ _ _ _ _ _ _)
-           @ ap (fun x => _ o x) (commutes T _ _ m)
-           @ (associativity_sym _ _ _ _ _ _ _ _)
-           @ ap (fun x => x o _) (commutes T' _ _ m)
-           @ (associativity _ _ _ _ _ _ _ _).
-
-    Definition compose_commutes_sym s d (m : morphism C s d)
-    : morphism_of F'' m o CO s = CO d o morphism_of F m
-      := (associativity_sym _ _ _ _ _ _ _ _)
-           @ ap (fun x => x o _) (commutes_sym T' _ _ m)
-           @ (associativity _ _ _ _ _ _ _ _)
-           @ ap (fun x => _ o x) (commutes_sym T _ _ m)
-           @ (associativity_sym _ _ _ _ _ _ _ _).
-
-    Definition compose
-    : NaturalTransformation F F''
-      := Build_NaturalTransformation' F F''
-                                      (fun c => CO c)
-                                      compose_commutes
-                                      compose_commutes_sym.
-
-  End compose.
-  End composition.
-Module Export NaturalTransformationCompositionCoreNotations.
-
-  Infix "o" := compose : natural_transformation_scope.
-End NaturalTransformationCompositionCoreNotations.
-End Core.
-
-End Composition.
-
-End NaturalTransformation.
-
-End categories.
-
-Set Universe Polymorphism.
-
-Section path_natural_transformation.
-
-  Context `{Funext}.
-  Variable C : PreCategory.
-
-  Variable D : PreCategory.
-  Variables F G : Functor C D.
-
-  Global Instance trunc_natural_transformation
-  : IsHSet (NaturalTransformation F G).
-
-admit.
-Defined.
-  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
-    : components_of T == components_of U
-      -> 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.
-
-Module Export Identity.
-Set Universe Polymorphism.
-
-Set Implicit Arguments.
-Local Open Scope morphism_scope.
-
-Local Open Scope path_scope.
-Section identity.
-
-  Variable C : PreCategory.
-  Variable D : PreCategory.
-
-  Section generalized.
-
-    Variables F G : Functor C D.
-    Hypothesis HO : object_of F = object_of G.
-    Hypothesis HM : transport (fun GO => forall s d,
-                                           morphism C s d
-                                           -> morphism D (GO s) (GO d))
-                              HO
-                              (morphism_of F)
-                    = morphism_of G.
-    Local Notation CO c := (transport (fun GO => morphism D (F c) (GO c))
-                                      HO
-                                      (identity (F c))).
-
-    Definition generalized_identity_commutes s d (m : morphism C s d)
-    : CO d o morphism_of F m = morphism_of G m o CO s.
-
-    Proof.
-      case HM.
-case HO.
-      exact (left_identity _ _ _ _ @ (right_identity _ _ _ _)^).
-    Defined.
-    Definition generalized_identity_commutes_sym s d (m : morphism C s d)
-    : morphism_of G m o CO s = CO d o morphism_of F m.
-
-admit.
-Defined.
-    Definition generalized_identity
-    : NaturalTransformation F G
-      := Build_NaturalTransformation'
-           F G
-           (fun c => CO c)
-           generalized_identity_commutes
-           generalized_identity_commutes_sym.
-
-  End generalized.
-  Definition identity (F : Functor C D)
-  : NaturalTransformation F F
-    := Eval simpl in @generalized_identity F F 1 1.
-
-End identity.
-Module Export NaturalTransformationIdentityNotations.
-
-  Notation "1" := (identity _) : natural_transformation_scope.
-End NaturalTransformationIdentityNotations.
-End Identity.
-
-Module Export Laws.
-Import HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Composition_DOT_Core.HoTT.categories.
-Set Universe Polymorphism.
-
-Local Open Scope natural_transformation_scope.
-Section natural_transformation_identity.
-
-  Context `{fs : Funext}.
-  Variable C : PreCategory.
-
-  Variable D : PreCategory.
-
-  Lemma left_identity (F F' : Functor C D)
-        (T : NaturalTransformation F F')
-  : 1 o T = T.
-
-  Proof.
-    path_natural_transformation; auto with morphism.
-  Qed.
-
-  Lemma right_identity (F F' : Functor C D)
-        (T : NaturalTransformation F F')
-  : T o 1 = T.
-
-  Proof.
-    path_natural_transformation; auto with morphism.
-  Qed.
-End natural_transformation_identity.
-Section associativity.
-
-  Section nt.
-
-    Context `{fs : Funext}.
-    Definition associativity
-               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.
-  End nt.
-End associativity.
-End Laws.
-
-Module Export FunctorCategory.
-Module Export Core.
-Import HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Composition_DOT_Core.HoTT.categories.
-Set Universe Polymorphism.
-
-Section functor_category.
-
-  Context `{Funext}.
-  Variable C : PreCategory.
-
-  Variable D : PreCategory.
-
-  Definition functor_category : PreCategory
-    := @Build_PreCategory (Functor C D)
-                          (@NaturalTransformation C D)
-                          (@identity C D)
-                          (@compose C D)
-                          (@associativity _ C D)
-                          (@left_identity _ C D)
-                          (@right_identity _ C D)
-                          _.
-
-End functor_category.
-Module Export FunctorCategoryCoreNotations.
-
-  Notation "C -> D" := (functor_category C D) : category_scope.
-End FunctorCategoryCoreNotations.
-End Core.
-
-End FunctorCategory.
-
-Module Export Morphisms.
-Set Universe Polymorphism.
-
-Set Implicit Arguments.
-
-Definition NaturalIsomorphism `{Funext} (C D : PreCategory) F G :=
-  @Isomorphic (C -> D) F G.
-
-Module Export FunctorCategoryMorphismsNotations.
-
-  Infix "<~=~>" := NaturalIsomorphism : natural_transformation_scope.
-End FunctorCategoryMorphismsNotations.
-End Morphisms.
-
-Module Export HSet.
-Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
-
-Global Existing Instance iss.
-End HSet.
-
-Module Export Core.
-Set Universe Polymorphism.
-
-Notation cat_of obj :=
-  (@Build_PreCategory obj
-                      (fun x y => x -> y)
-                      (fun _ x => x)
-                      (fun _ _ _ f g => f o g)%core
-                      (fun _ _ _ _ _ _ _ => idpath)
-                      (fun _ _ _ => idpath)
-                      (fun _ _ _ => idpath)
-                      _).
-
-Definition set_cat `{Funext} : PreCategory := cat_of hSet.
-Set Universe Polymorphism.
-
-Local Open Scope morphism_scope.
-
-Section hom_functor.
-
-  Context `{Funext}.
-  Variable C : PreCategory.
-  Local Notation obj_of c'c :=
-    (BuildhSet
-       (morphism
-          C
-          (fst (c'c : object (C^op * C)))
-          (snd (c'c : object (C^op * C))))
-       _).
-
-  Let hom_functor_morphism_of s's d'd (hf : morphism (C^op * C) s's d'd)
-  : morphism set_cat (obj_of s's) (obj_of d'd)
-    := fun g => snd hf o g o fst hf.
-
-  Definition hom_functor : Functor (C^op * C) set_cat.
-
-    refine (Build_Functor (C^op * C) set_cat
-                          (fun c'c => obj_of c'c)
-                          hom_functor_morphism_of
-                          _
-                          _);
-    subst hom_functor_morphism_of;
-    simpl; admit.
-  Defined.
-End hom_functor.
-Set Universe Polymorphism.
-
-Import Category.Dual Functor.Dual.
-Import Category.Prod Functor.Prod.
-Import Functor.Composition.Core.
-Import Functor.Identity.
-Set Universe Polymorphism.
-
-Local Open Scope functor_scope.
-Local Open Scope natural_transformation_scope.
-Section Adjunction.
-
-  Context `{Funext}.
-  Variable C : PreCategory.
-  Variable D : PreCategory.
-  Variable F : Functor C D.
-  Variable G : Functor D C.
-  Let Adjunction_Type := Eval simpl in hom_functor D o (F^op, 1) <~=~> hom_functor C o (1, G).
-
-End Adjunction.
-Undo.
-
-  Record AdjunctionHom :=
-    {
-      mate_of : @NaturalIsomorphism
-                  H
-                  (Category.Prod.prod (Category.Dual.opposite C) D)
-                  (@Core.set_cat H)
-                  (@compose
-                     (Category.Prod.prod (Category.Dual.opposite C) D)
-                     (Category.Prod.prod (Category.Dual.opposite D) D)
-                     (@Core.set_cat H) (@hom_functor H D)
-                     (@pair (Category.Dual.opposite C)
-                            (Category.Dual.opposite D) D D
-                            (@opposite C D F) (identity D)))
-                  (@compose
-                     (Category.Prod.prod (Category.Dual.opposite C) D)
-                     (Category.Prod.prod (Category.Dual.opposite C) C)
-                     (@Core.set_cat H) (@hom_functor H C)
-                     (@pair (Category.Dual.opposite C)
-                            (Category.Dual.opposite C) D C
-                            (identity (Category.Dual.opposite C)) G))
-    }.
-Fail End Adjunction.
-(* Error: Illegal application:
-The term "NaturalIsomorphism" of type
- "forall (H : Funext) (C D : PreCategory),
-  (C -> D)%category -> (C -> D)%category -> Type"
-cannot be applied to the terms
- "H" : "Funext"
- "(C ^op * D)%category" : "PreCategory"
- "set_cat" : "PreCategory"
- "hom_functor D o (F ^op, 1)" : "Functor (C ^op * D) set_cat"
- "hom_functor C o (1, G)" : "Functor (C ^op * D) set_cat"
-The 5th term has type "Functor (C ^op * D) set_cat"
-which should be coercible to "object (C ^op * D -> set_cat)".
-*)
diff --git a/test-suite/bugs/opened/3331.v b/test-suite/bugs/opened/3331.v
deleted file mode 100644
index 07504aed7..000000000
--- a/test-suite/bugs/opened/3331.v
+++ /dev/null
@@ -1,36 +0,0 @@
-(* File reduced by coq-bug-finder from original input, then from 6303 lines to 66 lines, then from 63 lines to 36 lines *)
-Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y :> A" := (@paths A x y) : type_scope.
-Arguments idpath {A a} , [A] a.
-Notation "x = y" := (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_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.
-Instance istrunc_paths (A : Type) n `{H : IsTrunc (trunc_S n) A} (x y : A) : IsTrunc n (x = y) := H x y.
-Notation Contr := (IsTrunc minus_two).
-Section groupoid_category.
-  Variable X : Type.
-  Context `{H : IsTrunc (trunc_S (trunc_S (trunc_S minus_two))) X}.
-  Goal X -> True.
-    intro d.
-    pose (_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))) as H'. (* success *)
-    clear H'.
-    compute in H.
-    change (forall (x y : X) (p q : x = y) (r s : p = q), Contr (r = s)) in H.
-    assert (H' := H).
-    pose proof (_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))) as X0. (* success *)
-    clear H' X0.
-    Fail pose (_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))). (* Toplevel input, characters 21-22:
-Error:
-Cannot infer this placeholder.
-Could not find an instance for "Contr (idpath = idpath)" in environment:
-
-X : Type
-H : forall (x y : X) (p q : x = y) (r s : p = q), Contr (r = s)
-d : X *)