- Add "Show Universes" to print information about universes during a proof.

- Remove dead code in evarconv.

2 files changed, 6 insertions, 99 deletions

diff --git a/test-suite/bugs/opened/HoTT_coq_020.v b/test-suite/bugs/opened/HoTT_coq_020.v
deleted file mode 100644
index ff73137a70..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_020.v
+++ /dev/null
@@ -1,95 +0,0 @@
-Set Implicit Arguments.
-
-Generalizable All Variables.
-
-Set Asymmetric Patterns.
-
-Polymorphic Record Category (obj : Type) :=
-  Build_Category {
-      Object :> _ := obj;
-      Morphism : obj -> obj -> Type;
-
-      Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
-    }.
-
-Polymorphic Record Functor objC (C : Category objC) objD (D : Category objD) :=
-  { ObjectOf :> objC -> objD }.
-
-Polymorphic Record NaturalTransformation objC C objD D (F G : Functor (objC := objC) C (objD := objD) D) :=
-  { ComponentsOf' :> forall c, D.(Morphism) (F.(ObjectOf) c) (G.(ObjectOf) c);
-    Commutes' : forall s d (m : C.(Morphism) s d), ComponentsOf' s = ComponentsOf' s }.
-
-Ltac present_obj from to :=
-  repeat match goal with
-           | [ _ : appcontext[from ?obj ?C] |- _ ] => progress change (from obj C) with (to obj C) in *
-           | [ |- appcontext[from ?obj ?C] ] => progress change (from obj C) with (to obj C) in *
-         end.
-
-Section NaturalTransformationComposition.
-  Set Universe Polymorphism.
-  Context `(C : @Category objC).
-  Context `(D : @Category objD).
-  Context `(E : @Category objE).
-  Variables F F' F'' : Functor C D.
-  Unset Universe Polymorphism.
-
-  Polymorphic Definition NTComposeT (T' : NaturalTransformation F' F'') (T : NaturalTransformation F F') :
-    NaturalTransformation F F''.
-    exists (fun c => Compose _ _ _ _ (T' c) (T c)).
-    progress present_obj @Morphism @Morphism. (* removing this line makes the error go away *)
-    intros. (* removing this line makes the error go away *)
-    admit.
-  Defined.
-End NaturalTransformationComposition.
-
-
-Polymorphic Definition FunctorCategory objC (C : Category objC) objD (D : Category objD) :
-  @Category (Functor C D)
-  := @Build_Category (Functor C D)
-                     (NaturalTransformation (C := C) (D := D))
-                     (NTComposeT (C := C) (D := D)).
-
-Polymorphic Definition Cat0 : Category Empty_set
-  := @Build_Category Empty_set
-                     (@eq _)
-                     (fun x => match x return _ with end).
-
-Polymorphic Definition FunctorFrom0 objC (C : Category objC) : Functor Cat0 C
-  := Build_Functor Cat0 C (fun x => match x with end).
-
-Section Law0.
-  Variable objC : Type.
-  Variable C : Category objC.
-
-  Set Printing All.
-  Set Printing Universes.
-  Set Printing Existential Instances.
-
-  Fail Polymorphic Definition ExponentialLaw0Functor_Inverse_ObjectOf' : Object (@FunctorCategory Empty_set Cat0 objC C).
-  (* In environment
-objC : Type (* Top.154 *)
-C : Category (* Top.155 Top.154 *) objC
-The term "objC" has type "Type (* Top.154 *)"
-while it is expected to have type "Type (* Top.184 *)"
-(Universe inconsistency: Cannot enforce Top.154 <= Set)). *)
-  Fail Admitted.
-
-  Fail Polymorphic Definition ExponentialLaw0Functor_Inverse_ObjectOf : Object (FunctorCategory Cat0 C).
-  Fail hnf.
-  Fail refine (@FunctorFrom0 _ _).
-    (* Toplevel input, characters 23-40:
-Error:
-In environment
-objC : Type (* Top.61069 *)
-C : Category (* Top.61069 Top.61071 *) objC
-The term
- "@FunctorFrom0 (* Top.61077 Top.61078 *) ?69 (* [objC, C] *)
-    ?70 (* [objC, C] *)" has type
- "@Functor (* Set Prop Top.61077 Top.61078 *) Empty_set Cat0
-    ?69 (* [objC, C] *) ?70 (* [objC, C] *)"
- while it is expected to have type
- "@Functor (* Set Prop Set Prop *) Empty_set Cat0 objC C".
-*)
-  Fail admit.
-  Fail Defined.
-End Law0.
diff --git a/test-suite/bugs/opened/HoTT_coq_062.v b/test-suite/bugs/opened/HoTT_coq_062.v
index 35d23efe98..e0ff5459cf 100644
--- a/test-suite/bugs/opened/HoTT_coq_062.v
+++ b/test-suite/bugs/opened/HoTT_coq_062.v
@@ -49,7 +49,8 @@ Local Open Scope equiv_scope.
 Definition equiv_path (A B : Type) (p : A = B) : A <~> B
   := BuildEquiv _ _ (transport (fun X:Type => X) p) admit.
 
-Class Univalence := { isequiv_equiv_path :> forall (A B : Type), IsEquiv (equiv_path A B) }.
+Class Univalence :=
+  isequiv_equiv_path :> forall (A B : Type), IsEquiv (equiv_path A B) .
 
 Section Univalence.
   Context `{Univalence}.
@@ -66,11 +67,13 @@ Defined.
 
 Definition p `{Univalence} : Bool = Bool := path_universe e.
 
-Theorem thm `{Univalence} : (forall A, ((A -> False) -> False) -> A) -> False.
+Theorem thm `{Univalence} : (forall A : Set, ((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)).
+  cut `{Univalence}; intros. pose proof (apD f p). 
+Admitted.
   (* ??? Toplevel input, characters 0-37:
 Error:
 Unable to satisfy the following constraints:
@@ -79,7 +82,6 @@ H : Univalence@{Top.144 Top.145 Top.146 Top.147 Top.148}
 f : forall (A : Type{Top.150}) (_ : forall _ : forall _ : A, False, False), A
 
 ?57 : "@IsEquiv@{Top.150 Top.145} Bool Bool (equiv_fun@{Set Set} Bool Bool e)" *)
-  Fail pose proof (apD f p).
 (* Toplevel input, characters 18-19:
 Error:
 In environment