Print universe names in subtyping error instead of Var(x).

3 files changed, 13 insertions, 10 deletions

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index e698ba9f8f..712eb21ee6 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -71,27 +71,26 @@ let int_or_no n = if Int.equal n 0 then str "no" else int n
 let print_basename sp = pr_global (ConstRef sp)
 
 let print_ref reduce ref udecl =
-  let typ, univs = Typeops.type_of_global_in_context (Global.env ()) ref in
+  let env = Global.env () in
+  let typ, univs = Typeops.type_of_global_in_context env ref in
   let inst = Univ.make_abstract_instance univs in
-  let bl = UnivNames.universe_binders_with_opt_names ref udecl in
+  let bl = UnivNames.universe_binders_with_opt_names (Environ.universes_of_global env ref) udecl in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
   let typ = EConstr.of_constr typ in
   let typ =
     if reduce then
-      let env = Global.env () in
       let ctx,ccl = Reductionops.splay_prod_assum env sigma typ
       in EConstr.it_mkProd_or_LetIn ccl ctx
     else typ in
   let variance = match ref with
     | VarRef _ | ConstRef _ -> None
     | IndRef (ind,_) | ConstructRef ((ind,_),_) ->
-      let mind = Environ.lookup_mind ind (Global.env ()) in
+      let mind = Environ.lookup_mind ind env in
       begin match mind.Declarations.mind_universes with
         | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> None
         | Declarations.Cumulative_ind cumi -> Some (Univ.ACumulativityInfo.variance cumi)
       end
   in
-  let env = Global.env () in
   let inst =
     if Global.is_polymorphic ref
     then Printer.pr_universe_instance sigma inst
@@ -571,7 +570,7 @@ let print_constant with_values sep sp udecl =
   in
   let ctx =
     UState.of_binders
-      (UnivNames.universe_binders_with_opt_names (ConstRef sp) udecl)
+      (UnivNames.universe_binders_with_opt_names (Declareops.constant_polymorphic_context cb) udecl)
   in
   let env = Global.env () and sigma = Evd.from_ctx ctx in
   let pr_ltype = pr_ltype_env env sigma in
diff --git a/printing/printer.ml b/printing/printer.ml
index 8227933433..7ce08ed6bc 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -250,7 +250,7 @@ let pr_universe_instance_constraints evd inst csts =
   let pcsts = if Constraint.is_empty csts then mt()
     else str " |= " ++
          prlist_with_sep (fun () -> str "," ++ spc())
-           (fun (u,d,v) -> prlev u ++ pr_constraint_type d ++ prlev v)
+           (fun (u,d,v) -> hov 0 (prlev u ++ pr_constraint_type d ++ prlev v))
            (Constraint.elements csts)
   in
   str"@{" ++ Instance.pr prlev inst ++ pcsts ++ str"}"
diff --git a/printing/printmod.ml b/printing/printmod.ml
index cc40c74998..2c3ab46670 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -119,7 +119,9 @@ let print_mutual_inductive env mind mib udecl =
     | BiFinite -> "Variant"
     | CoFinite -> "CoInductive"
   in
-  let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) udecl in
+  let bl = UnivNames.universe_binders_with_opt_names
+      (Declareops.inductive_polymorphic_context mib) udecl
+  in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
   hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
          Printer.pr_cumulative
@@ -157,7 +159,9 @@ let print_record env mind mib udecl =
   let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in
   let fields = get_fields cstrtype in
   let envpar = push_rel_context params env in
-  let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind,0)) udecl in
+  let bl = UnivNames.universe_binders_with_opt_names (Declareops.inductive_polymorphic_context mib)
+      udecl
+  in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
   let keyword =
     let open Declarations in
@@ -296,7 +300,7 @@ let print_body is_impl extent env mp (l,body) =
       (match extent with
          | OnlyNames -> mt ()
          | WithContents ->
-            let bl = UnivNames.universe_binders_with_opt_names (ConstRef (Constant.make2 mp l)) None in
+            let bl = UnivNames.universe_binders_with_opt_names ctx None in
             let sigma = Evd.from_ctx (UState.of_binders bl) in
 	    str " :" ++ spc () ++
             hov 0 (Printer.pr_ltype_env env sigma cb.const_type) ++