diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index f286f29b82af..3aae89a96664 100644
--- a/printing/ppconstr.ml
+++ b/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
diff --git a/printing/printer.mli b/printing/printer.mli
index a22da7849bc0..9549d9178a64 100644
--- a/printing/printer.mli
+++ b/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.
diff --git a/test-suite/bugs/bug_17298.v b/test-suite/bugs/bug_17298.v
index f513a7555468..49704d509e73 100644
--- a/test-suite/bugs/bug_17298.v
+++ b/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.
diff --git a/test-suite/output/DeclareSort.out b/test-suite/output/DeclareSort.out
index 38c39e98d7d9..511311778624 100644
--- a/test-suite/output/DeclareSort.out
+++ b/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}"
diff --git a/test-suite/output/NotationsSigma.out b/test-suite/output/NotationsSigma.out
index e9ad0453d764..0e4df87148e8 100644
--- a/test-suite/output/NotationsSigma.out
+++ b/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
diff --git a/test-suite/output/SortQuality.out b/test-suite/output/SortQuality.out
index dd7391926d9b..1bb402a6df70 100644
--- a/test-suite/output/SortQuality.out
+++ b/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 ; _}
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 22a1095b6e20..e4d62b0b8d42 100644
--- a/test-suite/output/UnivBinders.out
+++ b/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}
diff --git a/test-suite/output/UnivNotations.out b/test-suite/output/UnivNotations.out
index 9680f515c8d6..3d192a446502 100644
--- a/test-suite/output/UnivNotations.out
+++ b/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
   
   ============================
diff --git a/test-suite/output/check_minim_univs.out b/test-suite/output/check_minim_univs.out
new file mode 100644
index 000000000000..9042e0727261
--- /dev/null
+++ b/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} |=  *)
diff --git a/test-suite/output/check_minim_univs.v b/test-suite/output/check_minim_univs.v
new file mode 100644
index 000000000000..dcad4bfb8337
--- /dev/null
+++ b/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} *)
diff --git a/test-suite/output/nested_eliminators.out b/test-suite/output/nested_eliminators.out
index 1f47c2cfda52..0c752fef0c19 100644
--- a/test-suite/output/nested_eliminators.out
+++ b/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}
diff --git a/test-suite/output/prim_array.out b/test-suite/output/prim_array.out
index bf20b3eca6b6..691c0c659ed3 100644
--- a/test-suite/output/prim_array.out
+++ b/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 *)
diff --git a/test-suite/output/sort_poly_elab.out b/test-suite/output/sort_poly_elab.out
index 12897bc7161c..ace1a807290b 100644
--- a/test-suite/output/sort_poly_elab.out
+++ b/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 |=  *)
 
diff --git a/test-suite/output/unidecls.out b/test-suite/output/unidecls.out
index 5ee18fc43a01..94e095fc1815 100644
--- a/test-suite/output/unidecls.out
+++ b/test-suite/output/unidecls.out
@@ -88,7 +88,12 @@ a < decls.a
 secfoo2 < a
 Arg.u < Fn.v
 
-id@{Set} nat
+id@{unidecls.17} nat
      : nat -> nat
+(* {unidecls.17} |= Set <= unidecls.17
+Minimized universes:
+ unidecls.17 := Set
+Normalized constraints:
+  *)
 id@{Set}
      : forall A : Set, A -> A
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 50fe68a8abe1..e2412251dc70 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -184,13 +184,16 @@ let show_top_evars ~proof =
   let given_up = Evar.Set.elements @@ Evd.given_up sigma in
   pr_evars_int sigma ~shelf ~given_up 1 (Evd.undefined_map sigma)
 
-let show_universes ~proof =
-  let Proof.{ goals; sigma; poly } = Proof.data proof in
+let show_universes_aux ~poly sigma =
   let ctx = Evd.sort_context_set (Evd.minimize_universes ~poly sigma) in
   UState.pr (Evd.ustate sigma) ++ fnl () ++
   v 1 (str "Normalized constraints:" ++ cut() ++
        UnivGen.pr_sort_context (Evd.sort_printer sigma) ctx)
 
+let show_universes ~proof =
+  let Proof.{ sigma; poly } = Proof.data proof in
+  show_universes_aux ~poly sigma
+
 (* Simulate the Intro(s) tactic *)
 let show_intro ~proof all =
   let open EConstr in
@@ -2100,23 +2103,7 @@ let check_may_eval env sigma redexp rc =
   let sigma, c = Pretyping.understand_tcc env sigma gc in
   let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
   Evarconv.check_problems_are_solved env sigma;
-  let sigma = Evd.minimize_universes sigma in
-  let (qs, us), csts as uctx = Evd.sort_context_set sigma in
-  let { Environ.uj_val=c; uj_type=ty; } =
-    if Evarutil.has_undefined_evars sigma c
-    || List.exists (Context.Named.Declaration.exists (Evarutil.has_undefined_evars sigma))
-         (EConstr.named_context env)
-    then
-      Evarutil.j_nf_evar sigma (Retyping.get_judgment_of env sigma c)
-    else
-      let env = Evarutil.nf_env_evar sigma env in
-      let env = Environ.set_qualities (Evd.elim_graph sigma) env in
-      let env = Environ.set_universes (Evd.universes sigma) env in
-      let env = Safe_typing.push_private_constants env (Evd.seff_private @@ Evd.eval_side_effects sigma) in
-      let c = EConstr.to_constr sigma c in
-      (* OK to call kernel which does not support evars *)
-      Environ.on_judgment EConstr.of_constr (Arguments_renaming.rename_typing env c)
-  in
+  let { Environ.uj_val=c; uj_type=ty; } = Retyping.get_judgment_of env sigma c in
   let sigma, c = match redexp with
     | None -> sigma, c
     | Some r ->
@@ -2133,7 +2120,39 @@ let check_may_eval env sigma redexp rc =
     pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma l
   in
   let hdr = if Option.has_some redexp then str "     = " else mt() in
-  hdr ++ pp ++ Printer.pr_sort_context_set sigma uctx
+  let ppunivs =
+    let ctx = Evd.sort_context_set sigma in
+    (* NB: flags only used for collapse_sort_variables
+       XXX get current option value instead of default? *)
+    let sigma' = Evd.minimize_universes ~poly:PolyFlags.default sigma in
+    let ctx' = Evd.sort_context_set sigma' in
+    let defsorts = Sorts.QVar.Set.(elements @@ diff (fst (fst ctx)) (fst (fst ctx'))) in
+    let defunivs = Univ.Level.Set.(elements @@ diff (snd (fst ctx)) (snd (fst ctx'))) in
+    let pr_defsort q =
+      Termops.pr_evd_qvar sigma q ++ str " := " ++
+      Termops.pr_evd_quality sigma' (UState.nf_qvar (Evd.ustate sigma') q)
+    in
+    let pr_defuniv u =
+      Termops.pr_evd_level sigma u ++ str " := " ++
+      Univ.Universe.pr (Termops.pr_evd_level sigma)
+        (UState.nf_universe (Evd.ustate sigma') (Univ.Universe.make u))
+    in
+    if !PrintingFlags.print_universes && not (UnivGen.is_empty_sort_context ctx) then
+      fnl() ++
+      (Printer.pr_in_comment
+         (UnivGen.pr_sort_context (Evd.sort_printer sigma) ctx ++ fnl() ++
+          (if List.is_empty defsorts then mt() else
+             v 1 (str "Collapsed sorts:" ++ cut() ++ prlist_with_sep cut pr_defsort defsorts)
+             ++ fnl()) ++
+          (if List.is_empty defunivs then mt() else
+             v 1 (str "Minimized universes:" ++ cut() ++ prlist_with_sep cut pr_defuniv defunivs)
+             ++ fnl()) ++
+          v 1
+            (str "Normalized constraints:" ++ cut() ++
+             UnivGen.pr_sort_context (Evd.sort_printer sigma) ctx')))
+    else mt()
+  in
+  hdr ++ pp ++ ppunivs
 
 let vernac_check_may_eval ~pstate redexp glopt rc =
   let glopt = query_command_selector glopt in