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

- Remove dead code in evarconv.

2 files changed, 15 insertions, 13 deletions

diff --git a/test-suite/bugs/opened/HoTT_coq_020.v b/test-suite/bugs/closed/HoTT_coq_020.v
index ff73137a70..b16c1df2bd 100644
--- a/test-suite/bugs/opened/HoTT_coq_020.v
+++ b/test-suite/bugs/closed/HoTT_coq_020.v
@@ -20,7 +20,7 @@ Polymorphic Record NaturalTransformation objC C objD D (F G : Functor (objC := o
     Commutes' : forall s d (m : C.(Morphism) s d), ComponentsOf' s = ComponentsOf' s }.
 
 Ltac present_obj from to :=
-  repeat match goal with
+  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.
@@ -36,7 +36,7 @@ Section NaturalTransformationComposition.
   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 *)
+    repeat progress present_obj @Morphism @Morphism. (* removing this line makes the error go away *)
     intros. (* removing this line makes the error go away *)
     admit.
   Defined.
@@ -65,18 +65,19 @@ Section Law0.
   Set Printing Universes.
   Set Printing Existential Instances.
 
-  Fail Polymorphic Definition ExponentialLaw0Functor_Inverse_ObjectOf' : Object (@FunctorCategory Empty_set Cat0 objC C).
+  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.
+  Admitted.
+
+  Polymorphic Definition ExponentialLaw0Functor_Inverse_ObjectOf : Object (FunctorCategory Cat0 C).
+    hnf.
+    refine (@FunctorFrom0 _ _).
 
-  Fail Polymorphic Definition ExponentialLaw0Functor_Inverse_ObjectOf : Object (FunctorCategory Cat0 C).
-  Fail hnf.
-  Fail refine (@FunctorFrom0 _ _).
     (* Toplevel input, characters 23-40:
 Error:
 In environment
@@ -90,6 +91,5 @@ The term
  while it is expected to have type
  "@Functor (* Set Prop Set Prop *) Empty_set Cat0 objC C".
 *)
-  Fail admit.
-  Fail Defined.
+  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