Don't print term with minimized universes in Check/Eval

printing/ppconstr.ml

@@ -232,7 +232,7 @@ let pr_quality_univ (q, l) = match q with
   | None -> pr_univ l
   | Some q ->  pr_quality_expr q ++ spc() ++ str ";" ++ spc () ++ pr_univ l
 
-let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
+let pr_univ_annot pr x = hov 2 (str "@{" ++ pr x ++ str "}")
 
 let pr_sort_expr : sort_expr -> Pp.t = function
   | None, UNamed [CSProp, 0] -> tag_type (str "SProp")
@@ -269,7 +269,9 @@ let pr_reference qid =
   else pr_qualid qid
 
 let pr_cref ref us =
-  pr_reference ref ++ pr_universe_instance us
+  (* for some reason the hov 0 around an reference without univ instance makes printing worse *)
+  if Option.has_some us then hov 0 (pr_reference ref ++ pr_universe_instance us)
+  else pr_reference ref
 
 let pr_expl_args pr lev_after (a,expl) =
   match expl with

printing/printer.mli

@@ -21,6 +21,8 @@ open Notation_term
 
 val print_goal_tag_opt_name : string list
 
+val pr_in_comment : Pp.t -> Pp.t
+
 (** Terms *)
 
 (** Printers for terms.

test-suite/bugs/bug_17298.v

@@ -1,18 +1,18 @@
+(* this test used to check that Check used to correct rule for when to
+   recheck with the kernel (and avoided sending evars to the kernel),
+   but now Check never rechecks with the kernel so it's always correct. *)
 Goal True.
 let c := open_constr:(_) in
 let _ := open_constr:(c : nat) in
 pose (x:=c);
 pose (y := c).
 
-(* evars remain, do not use the kernel *)
 Check (eq_refl : x = y).
 
-(* evars remain, since we don't recheck with the kernel this is accepted *)
 Check (ltac:(exact_no_check (@eq_refl nat 0)) : x = y).
 
-(* no evars, check that the kernel got the normalized env *)
 Check (eq_refl : x = 0).
 
-Fail Check (ltac:(let _ := open_constr:(eq_refl : x = 0) in
-                  exact_no_check (@eq_refl nat 1)) : x = 0).
+Check (ltac:(let _ := open_constr:(eq_refl : x = 0) in
+             exact_no_check (@eq_refl nat 1)) : x = 0).
 Abort.

test-suite/output/DeclareSort.out

@@ -42,8 +42,18 @@ Expands to: Constant DeclareSort.foo
 Declared in library DeclareSort, line 19, characters 8-11
 foo@{SProp ; } : Type@{S1 ; Set} -> SProp
      : Type@{S1 ; Set} -> SProp
+(* {DeclareSort.25} |= Set < DeclareSort.25
+Minimized universes:
+ DeclareSort.25 := Set+1
+Normalized constraints:
+  *)
 foo@{Type ; } : Type@{S1 ; Set} -> Set
      : Type@{S1 ; Set} -> Set
+(* {DeclareSort.26} |= Set < DeclareSort.26
+Minimized universes:
+ DeclareSort.26 := Set+1
+Normalized constraints:
+  *)
 File "./output/DeclareSort.v", line 30, characters 11-14:
 The command has indeed failed with message:
 The term "foo@{α6 ; }" has type "Type@{S1 ; Set} -> Type@{α6 ; Set}"

test-suite/output/NotationsSigma.out

@@ -33,8 +33,8 @@ where
 where
 ?T : [pat : nat * ?T |- Type] (pat cannot be used)
 {'(x, y) : nat * nat & x = 1 & y = 0}
-     : Set
+     : Type
 {'(x, _) : nat * nat & x = 1}
-     : Set
+     : Type
 {'(x, y) : nat * nat & x = 1 & y = 0}
-     : Set
+     : Type

test-suite/output/SortQuality.out

@@ -6,9 +6,13 @@ A
      : Type@{s ; _}
 A
      : Type@{s ; u}
-(* {s}; {u} |=  *)
+(* {s}; {u} |= 
+Normalized constraints:
+ {s}; {u} |=  *)
 A
      : Type@{s ; u}
-(* {s}; {u} |=  *)
+(* {s}; {u} |= 
+Normalized constraints:
+ {s}; {u} |=  *)
 A
      : Type@{s ; _}

test-suite/output/UnivBinders.out

@@ -50,10 +50,14 @@ Type@{u} -> Type@{v} -> Type@{uu}
 (* uu u v |=  *)
 Type@{i} -> Type@{j}
      : Type@{max(i+1,j+1)}
-(* {j i} |=  *)
+(* {j i} |= 
+Normalized constraints:
+ {j i} |=  *)
      = Type@{i} -> Type@{j}
      : Type@{max(i+1,j+1)}
-(* {j i} |=  *)
+(* {j i} |= 
+Normalized constraints:
+ {j i} |=  *)
 mono = Type@{mono.uu}
      : Type@{mono.uu+1}
 mono
@@ -213,7 +217,9 @@ foo@{i} = Type@{M.i} -> Type@{i}
 (* i |=  *)
 Type@{u0} -> Type@{UnivBinders.86}
      : Type@{max(u0+1,UnivBinders.86+1)}
-(* {UnivBinders.86} |=  *)
+(* {UnivBinders.86} |= 
+Normalized constraints:
+ {UnivBinders.86} |=  *)
 bind_univs.mono = Type@{bind_univs.mono.u}
      : Type@{bind_univs.mono.u+1}
 bind_univs.poly@{u} = Type@{u}

test-suite/output/UnivNotations.out

@@ -15,10 +15,15 @@ UnivNotations.24).
   forall A : Type, A -> ! A
 foo Type@{UnivNotations.27} nat
      : Type@{foo.u1}
-(* {UnivNotations.27} |= UnivNotations.27 < foo.u0 *)
+(* {UnivNotations.27} |= UnivNotations.27 < foo.u0
+                         Set <= UnivNotations.27
+Normalized constraints:
+ {UnivNotations.27} |= UnivNotations.27 < foo.u0 *)
 foo Type@{s ; Set} S
      : Type@{foo.u1}
-(* {} |= Set < foo.u0 *)
+(* {} |= Set < foo.u0
+Normalized constraints:
+ {} |= Set < foo.u0 *)
 1 goal
 
   ============================

test-suite/output/check_minim_univs.out

@@ -0,0 +1,7 @@
+abc@{α4 ; check_minim_univs.24}
+     : Type@{check_minim_univs.24+1}
+(* {α4}; {check_minim_univs.24} |= 
+Collapsed sorts:
+ α4 := Type
+Normalized constraints:
+ {check_minim_univs.24} |=  *)

test-suite/output/check_minim_univs.v

@@ -0,0 +1,9 @@
+(* from #20508 *)
+
+#[universes(polymorphic=yes)]
+Definition abc@{s;u|} := Type@{s;u}.
+Inductive SUnit : SProp := stt.
+Definition xyz : abc := SUnit. (* works as expected, abc is sort-polymorphic *)
+Set Printing Universes.
+Check @abc.
+(* prints abc@{Type | test.294} : Type@{test.294+1} *)

test-suite/output/nested_eliminators.out

@@ -1106,7 +1106,8 @@ All2i_bis_all_all@{α α0 α1 α2 ; u u0 u1 u2 u3 u4 u5 u6}
     All2i_bis_nil_all_all : forall (c : C) (p : PC c),
                             PPC c p ->
                             All2i_bis_all_all@{α α0 α1 α2 ; u u0 u1 u2 u3 u4
-                              u5 u6} A B C PC PPC R PR PPR n nil nil
+                                               u5 u6}
+                              A B C PC PPC R PR PPR n nil nil
                               (All2i_bis_nil A B C R n c)
                               (All2i_bis_nil_all@{α α0 ; u u0 u1 u2 u3 u4} A
                                  B C PC R PR n c p)
@@ -1119,10 +1120,12 @@ All2i_bis_all_all@{α α0 α1 α2 ; u u0 u1 u2 u3 u4 u5 u6}
                                        A B C PC R PR 
                                        (S n) lA lB a0),
                              All2i_bis_all_all@{α α0 α1 α2 ; u u0 u1 u2 u3 u4
-                               u5 u6} A B C PC PPC R PR PPR 
+                                                u5 u6}
+                               A B C PC PPC R PR PPR 
                                (S n) lA lB a0 a1 ->
                              All2i_bis_all_all@{α α0 α1 α2 ; u u0 u1 u2 u3 u4
-                               u5 u6} A B C PC PPC R PR PPR n 
+                                                u5 u6}
+                               A B C PC PPC R PR PPR n 
                                (cons a lA) (cons b lB)
                                (All2i_bis_cons A B C R n a b lA lB r a0)
                                (All2i_bis_cons_all@{α α0 ; u u0 u1 u2 u3 u4}

test-suite/output/prim_array.out

@@ -2,8 +2,23 @@
      : array nat
 [| 1; 2; 3 | 0 : nat |]
      : array nat
-[| | 0 : nat |]@{Set}
-     : array@{Set} nat
+[| | 0 : nat |]@{prim_array.26}
+     : array@{prim_array.26} nat
+(* {prim_array.26 prim_array.25} |= Set <= prim_array.25
+                                    Set <= prim_array.26
+Minimized universes:
+ prim_array.26 := Set
+ prim_array.25 := Set
+Normalized constraints:
+  *)
 [| bool; list nat | nat : Set |]@{prim_array.29}
      : array@{prim_array.29} Set
-(* {prim_array.29} |= Set < prim_array.29 *)
+(* {prim_array.29 prim_array.28 prim_array.27} |=
+     Set < prim_array.27
+     Set < prim_array.29
+     Set <= prim_array.28
+Minimized universes:
+ prim_array.28 := Set
+ prim_array.27 := Set+1
+Normalized constraints:
+ {prim_array.29} |= Set < prim_array.29 *)

test-suite/output/sort_poly_elab.out

@@ -16,17 +16,41 @@ Declared in library sort_poly_elab, line 14, characters 13-19
 :
 @eq Type@{sort_poly_elab.26} q1 tU@{Type ; }
      : @eq Type@{sort_poly_elab.26} q1 tU@{Type ; }
-(* {sort_poly_elab.26} |= U < sort_poly_elab.26 *)
+(* {sort_poly_elab.27 sort_poly_elab.26 sort_poly_elab.25} |=
+     U < sort_poly_elab.26
+     sort_poly_elab.26 < sort_poly_elab.25
+     sort_poly_elab.26 < sort_poly_elab.27
+Minimized universes:
+ sort_poly_elab.27 := sort_poly_elab.26+1
+ sort_poly_elab.25 := sort_poly_elab.26+1
+Normalized constraints:
+ {sort_poly_elab.26} |= U < sort_poly_elab.26 *)
 @eq_refl Type@{sort_poly_elab.29} q2
 :
 @eq Type@{sort_poly_elab.29} q2 tU@{Type ; }
      : @eq Type@{sort_poly_elab.29} q2 tU@{Type ; }
-(* {sort_poly_elab.29} |= U < sort_poly_elab.29 *)
+(* {sort_poly_elab.30 sort_poly_elab.29 sort_poly_elab.28} |=
+     U < sort_poly_elab.29
+     sort_poly_elab.29 < sort_poly_elab.28
+     sort_poly_elab.29 < sort_poly_elab.30
+Minimized universes:
+ sort_poly_elab.30 := sort_poly_elab.29+1
+ sort_poly_elab.28 := sort_poly_elab.29+1
+Normalized constraints:
+ {sort_poly_elab.29} |= U < sort_poly_elab.29 *)
 @eq_refl Type@{sort_poly_elab.32} q3
 :
 @eq Type@{sort_poly_elab.32} q3 tU@{Type ; }
      : @eq Type@{sort_poly_elab.32} q3 tU@{Type ; }
-(* {sort_poly_elab.32} |= U < sort_poly_elab.32 *)
+(* {sort_poly_elab.33 sort_poly_elab.32 sort_poly_elab.31} |=
+     U < sort_poly_elab.32
+     sort_poly_elab.32 < sort_poly_elab.31
+     sort_poly_elab.32 < sort_poly_elab.33
+Minimized universes:
+ sort_poly_elab.33 := sort_poly_elab.32+1
+ sort_poly_elab.31 := sort_poly_elab.32+1
+Normalized constraints:
+ {sort_poly_elab.32} |= U < sort_poly_elab.32 *)
 exfalso@{α ; u} : forall (A : Type@{α ; u}) (_ : False), A
 (* α ; u |=  *)
 
@@ -130,7 +154,16 @@ fun A : SProp =>
        @eq (forall (_ : A) (_ : A), Box@{SProp Type ; sort_poly_elab.62} A)
          (t1@{SProp Type ; sort_poly_elab.62} A)
          (t2@{SProp Type ; sort_poly_elab.62} A)
-(* {sort_poly_elab.62} |=  *)
+(* {sort_poly_elab.64 sort_poly_elab.63 sort_poly_elab.62 sort_poly_elab.61} |=
+     sort_poly_elab.62 <= sort_poly_elab.61
+     sort_poly_elab.62 <= sort_poly_elab.64
+     sort_poly_elab.63 = sort_poly_elab.62
+Minimized universes:
+ sort_poly_elab.64 := sort_poly_elab.62
+ sort_poly_elab.63 := sort_poly_elab.62
+ sort_poly_elab.61 := sort_poly_elab.62
+Normalized constraints:
+ {sort_poly_elab.62} |=  *)
 fun A : SProp =>
 @eq_refl (Box@{SProp Type ; sort_poly_elab.66} (forall (_ : A) (_ : A), A))
   (box@{SProp Type ; sort_poly_elab.66} (forall (_ : A) (_ : A), A)
@@ -147,7 +180,17 @@ fun A : SProp =>
             (t1'@{SProp ; sort_poly_elab.67} A))
          (box@{SProp Type ; sort_poly_elab.66} (forall (_ : A) (_ : A), A)
             (t2'@{SProp ; sort_poly_elab.69} A))
-(* {sort_poly_elab.69 sort_poly_elab.67 sort_poly_elab.66} |=  *)
+(* {sort_poly_elab.70 sort_poly_elab.69 sort_poly_elab.68 sort_poly_elab.67
+    sort_poly_elab.66 sort_poly_elab.65} |=
+     sort_poly_elab.66 <= sort_poly_elab.65
+     sort_poly_elab.66 <= sort_poly_elab.70
+     sort_poly_elab.68 = sort_poly_elab.66
+Minimized universes:
+ sort_poly_elab.70 := sort_poly_elab.66
+ sort_poly_elab.68 := sort_poly_elab.66
+ sort_poly_elab.65 := sort_poly_elab.66
+Normalized constraints:
+ {sort_poly_elab.69 sort_poly_elab.67 sort_poly_elab.66} |=  *)
 ignore@{α ; u} : forall {A : Type@{α ; u}} (_ : A), unit
 (* α ; u |=  *)
 
@@ -194,14 +237,24 @@ x : P (v@{Type ; sort_poly_elab.84} nat true)
 The term "x" has type "P (v@{Type ; sort_poly_elab.84} nat true)"
 while it is expected to have type
  "P (v@{Type ; sort_poly_elab.86} nat false)".
-fun (A : SProp) (P : forall _ : A, Type@{sort_poly_elab.91})
+fun (A : SProp) (P : forall _ : A, Type@{α63 ; sort_poly_elab.91})
   (x : P (v@{SProp ; sort_poly_elab.90} A true)) =>
 x : P (v@{SProp ; sort_poly_elab.92} A false)
-     : forall (A : SProp) (P : forall _ : A, Type@{sort_poly_elab.91})
+     : forall (A : SProp) (P : forall _ : A, Type@{α63 ; sort_poly_elab.91})
          (_ : P (v@{SProp ; sort_poly_elab.90} A true)),
        P (v@{SProp ; sort_poly_elab.92} A false)
-(* {sort_poly_elab.92 sort_poly_elab.91 sort_poly_elab.90 sort_poly_elab.88} |=
-      *)
+(* {α63}; {sort_poly_elab.92 sort_poly_elab.91 sort_poly_elab.90
+           sort_poly_elab.89 sort_poly_elab.88 sort_poly_elab.87} |=
+     sort_poly_elab.91 < sort_poly_elab.89
+     sort_poly_elab.88 <= sort_poly_elab.87
+     sort_poly_elab.89 <= sort_poly_elab.87
+Collapsed sorts:
+ α63 := Type
+Minimized universes:
+ sort_poly_elab.89 := sort_poly_elab.91+1
+ sort_poly_elab.87 := max(sort_poly_elab.88, sort_poly_elab.91+1)
+Normalized constraints:
+ {sort_poly_elab.92 sort_poly_elab.91 sort_poly_elab.90 sort_poly_elab.88} |=  *)
 zog@{α ; u} : forall _ : Type@{α ; u}, Type@{α ; u}
 (* α ; u |=  *)
 
@@ -742,6 +795,11 @@ match true@{Test ; } return testind'@{Test ; } with
 | false => testctor'@{Test ; }
 end
      : testind'@{Test ; }
+(* {sort_poly_elab.354} |= Set <= sort_poly_elab.354
+Minimized universes:
+ sort_poly_elab.354 := Set
+Normalized constraints:
+  *)
 unit@{α ; u} : Type@{α ; u}
 (* α ; u |=  *)
 
@@ -775,6 +833,9 @@ Expands to: Constant sort_poly_elab.Inductives.Foo
 Declared in library sort_poly_elab, line 531, characters 13-16
 Foo@{Type Prop ; }
      : forall _ : FooNat@{Type ; }, FooNat@{Prop ; }
+(* {} |= Type -> Prop
+Normalized constraints:
+  *)
 File "./output/sort_poly_elab.v", line 540, characters 2-30:
 The command has indeed failed with message:
 The quality constraints are inconsistent: cannot enforce Prop -> Type
@@ -840,7 +901,17 @@ fun (A : SProp) (x y : R6@{SProp ; } A) =>
        @eq (Conversion.Box@{SProp Type ; sort_poly_elab.365} A)
          (Conversion.box@{SProp Type ; sort_poly_elab.365} A (R6f1 _ x))
          (Conversion.box@{SProp Type ; sort_poly_elab.365} A (R6f1 _ y))
-(* {sort_poly_elab.365} |=  *)
+(* {sort_poly_elab.367 sort_poly_elab.366 sort_poly_elab.365
+    sort_poly_elab.364} |=
+     sort_poly_elab.365 <= sort_poly_elab.364
+     sort_poly_elab.365 <= sort_poly_elab.367
+     sort_poly_elab.366 = sort_poly_elab.365
+Minimized universes:
+ sort_poly_elab.367 := sort_poly_elab.365
+ sort_poly_elab.366 := sort_poly_elab.365
+ sort_poly_elab.364 := sort_poly_elab.365
+Normalized constraints:
+ {sort_poly_elab.365} |=  *)
 File "./output/sort_poly_elab.v", line 577, characters 10-17:
 The command has indeed failed with message:
 In environment
@@ -945,13 +1016,17 @@ sexists@{α ; u} may only be eliminated to produce values whose type is SProp or
 Arguments sexists A%_type_scope B%_function_scope
 Expands to: Inductive sort_poly_elab.Records.sexists
 Declared in library sort_poly_elab, line 612, characters 12-19
-sexists_ind@{Type ;
-sort_poly_elab.396}
-     : forall (A : Type@{sort_poly_elab.396}) (B : forall _ : A, Prop)
-         (P : Prop) (_ : forall (a : A) (_ : B a), P)
-         (_ : sexists@{Type ; sort_poly_elab.396} A B),
+sexists_ind@{α410 ; sort_poly_elab.396}
+     : forall (A : Type@{α410 ; sort_poly_elab.396}) 
+         (B : forall _ : A, Prop) (P : Prop)
+         (_ : forall (a : A) (_ : B a), P)
+         (_ : sexists@{α410 ; sort_poly_elab.396} A B),
        P
-(* {sort_poly_elab.396} |=  *)
+(* {α410}; {sort_poly_elab.396} |= 
+Collapsed sorts:
+ α410 := Type
+Normalized constraints:
+ {sort_poly_elab.396} |=  *)
 R8@{α α0 ; u} : Type@{α ; u+1}
 (* α α0 ; u |=  *)