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

- Remove dead code in evarconv.

8 files changed, 46 insertions, 42 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index be7e59a2de..89e1b41f39 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -101,6 +101,7 @@ type showable =
   | ShowNode
   | ShowScript
   | ShowExistentials
+  | ShowUniverses
   | ShowTree
   | ShowProofNames
   | ShowIntros of bool
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index e95aecca83..212d4af6d9 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -89,6 +89,7 @@ GEXTEND Gram
       | IDENT "Show"; IDENT "Node" -> VernacShow ShowNode
       | IDENT "Show"; IDENT "Script" -> VernacShow ShowScript
       | IDENT "Show"; IDENT "Existentials" -> VernacShow ShowExistentials
+      | IDENT "Show"; IDENT "Universes" -> VernacShow ShowUniverses
       | IDENT "Show"; IDENT "Tree" -> VernacShow ShowTree
       | IDENT "Show"; IDENT "Conjectures" -> VernacShow ShowProofNames
       | IDENT "Show"; IDENT "Proof" -> VernacShow ShowProof
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6f47a79caf..1c9796b4de 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -293,13 +293,6 @@ let exact_ise_stack2 env evd f sk1 sk2 =
   if Reductionops.Stack.compare_shape sk1 sk2 then
     ise_stack2 evd (List.rev sk1) (List.rev sk2)
   else UnifFailure (evd, (* Dummy *) NotSameHead)
-
-let eq_puniverses evd pbty f (x,u) (y,v) =
-  if f x y then 
-    try 
-      Success (Evd.set_eq_instances evd u v)
-    with Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e)
-  else UnifFailure (evd, NotSameHead)
     
 let rec evar_conv_x ts env evd pbty term1 term2 =
   let term1 = whd_head_evar evd term1 in
@@ -378,12 +371,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
   let rigids env evd sk term sk' term' =
     let b,univs = Universes.eq_constr_universes term term' in
       if b then
-	ise_and evd [(fun i -> 
-	  let cstrs = Universes.to_constraints (Evd.universes i) univs in
-	    try let i = Evd.add_constraints i cstrs in
-		  Success i
-	    with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
-		   (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')]
+       ise_and evd [(fun i ->
+         let cstrs = Universes.to_constraints (Evd.universes i) univs in
+           try Success (Evd.add_constraints i cstrs)
+           with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
+                  (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')]
       else UnifFailure (evd,NotSameHead)
   in
   let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM =
@@ -624,20 +616,6 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	| Construct _, Construct _ ->
 	  rigids env evd sk1 term1 sk2 term2
 
-	(*   ise_and evd *)
-	(*     [(fun i -> eq_puniverses i pbty eq_constant c1 c2); *)
-	(*      (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] *)
-
-	(* | Ind sp1, Ind sp2 -> *)
-	(*      ise_and evd *)
-	(*        [(fun i -> eq_puniverses i pbty eq_ind sp1 sp2); *)
-	(* 	(fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] *)
-
-	(* | Construct sp1, Construct sp2 -> *)
-	(*      ise_and evd *)
-	(*        [(fun i -> eq_puniverses i pbty eq_constructor sp1 sp2); *)
-	(* 	(fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] *)
-
 	| Fix ((li1, i1),(_,tys1,bds1 as recdef1)), Fix ((li2, i2),(_,tys2,bds2)) -> (* Partially applied fixs *)
 	  if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then
             ise_and evd [
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 5cad4806d4..6fa5b8896e 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -512,6 +512,7 @@ let rec pr_vernac = function
 	| ShowNode -> str"Show Node"
 	| ShowScript -> str"Show Script"
 	| ShowExistentials -> str"Show Existentials"
+	| ShowUniverses -> str"Show Universes"
 	| ShowTree -> str"Show Tree"
 	| ShowProofNames -> str"Show Conjectures"
 	| ShowIntros b -> str"Show " ++ (if b then str"Intros" else str"Intro")
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
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 39fe8f4ab3..d28445f177 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -245,14 +245,25 @@ let declare_assumptions idl is_coe k c imps impl_is_on nl =
       (ref',u')::refs, status' && status) ([],true) idl in
   List.rev refs, status
 
-let do_assumptions kind nl l =
+let do_assumptions (_, poly, _ as kind) nl l =
   let env = Global.env () in
   let evdref = ref (Evd.from_env env) in
+  let l = 
+    if poly then
+      (* Separate declarations so that A B : Type puts A and B in different levels. *)
+      List.fold_right (fun (is_coe,(idl,c)) acc ->
+        List.fold_right (fun id acc -> 
+	  (is_coe, ([id], c)) :: acc) idl acc)
+        l []
+    else l
+  in
   let _,l = List.fold_map (fun env (is_coe,(idl,c)) ->
     let (t,ctx),imps = interp_assumption evdref env [] c in
     let env =
       push_named_context (List.map (fun (_,id) -> (id,None,t)) idl) env in
-    (env,((is_coe,idl),t,(ctx,imps)))) env l in
+      (env,((is_coe,idl),t,(ctx,imps)))) 
+    env l 
+  in
   let evd = solve_remaining_evars all_and_fail_flags env Evd.empty !evdref in
   let l = List.map (on_pi2 (nf_evar evd)) l in
   snd (List.fold_left (fun (subst,status) ((is_coe,idl),t,(ctx,imps)) ->
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f043e8f162..27b53579f5 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -71,6 +71,15 @@ let show_top_evars () =
   let sigma = gls.Evd.sigma in
   msg_notice (pr_evars_int 1 (Evarutil.non_instantiated sigma))
 
+let show_universes () =
+  let pfts = get_pftreestate () in
+  let gls = Proof.V82.subgoals pfts in
+  let sigma = gls.Evd.sigma in
+  let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in
+  let cstrs = Univ.merge_constraints (Univ.ContextSet.constraints ctx) Univ.empty_universes in
+    msg_notice (Univ.pr_universe_context_set ctx);
+    msg_notice (str"Normalized constraints: " ++ Univ.pr_universes cstrs)
+
 let show_prooftree () =
   (* Spiwack: proof tree is currently not working *)
   ()
@@ -1619,6 +1628,7 @@ let vernac_show = function
   | ShowNode -> show_node ()
   | ShowScript -> Stm.show_script ()
   | ShowExistentials -> show_top_evars ()
+  | ShowUniverses -> show_universes ()
   | ShowTree -> show_prooftree ()
   | ShowProofNames ->
       msg_notice (pr_sequence pr_id (Pfedit.get_all_proof_names()))