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

6 files changed, 22 insertions, 20 deletions

diff --git a/engine/univNames.ml b/engine/univNames.ml
index ad91d31f87..1019f8f0c2 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -36,10 +36,6 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
 
 let empty_binders = Id.Map.empty
 
-let universe_binders_of_global ref : Name.t array =
-  try AUContext.names (Environ.universes_of_global (Global.env ()) ref)
-  with Not_found -> [||]
-
 let name_universe lvl =
   (** Best-effort naming from the string representation of the level. This is
       completely hackish and should be solved in upper layers instead. *)
@@ -55,8 +51,8 @@ let compute_instance_binders inst ubinders =
 
 type univ_name_list = Names.lname list
 
-let universe_binders_with_opt_names ref names =
-  let orig = universe_binders_of_global ref in
+let universe_binders_with_opt_names orig names =
+  let orig = AUContext.names orig in
   let orig = Array.to_list orig in
   let udecl = match names with
   | None -> orig
diff --git a/engine/univNames.mli b/engine/univNames.mli
index dc669f45d6..6e68153ac2 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -29,5 +29,5 @@ type univ_name_list = Names.lname list
     of [ref] by [univs] (skipping Anonymous). May error if the lengths mismatch.
 
     Otherwise return the bound universe names registered for [ref]. *)
-val universe_binders_with_opt_names : Names.GlobRef.t ->
+val universe_binders_with_opt_names : AUContext.t ->
   univ_name_list option -> universe_binders
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) ++
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index ad70f2067b..6c7117b513 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -894,17 +894,20 @@ let explain_not_match_error = function
       quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t2)
   | IncompatibleConstraints { got; expect } ->
       let open Univ in
-    (** FIXME: provide a proper naming for the bound variables *)
     let pr_auctx auctx =
+      let sigma = Evd.from_ctx
+          (UState.of_binders
+             (UnivNames.universe_binders_with_opt_names auctx None))
+      in
       let uctx = AUContext.repr auctx in
-      Printer.pr_universe_instance_constraints Evd.empty
+      Printer.pr_universe_instance_constraints sigma
         (UContext.instance uctx)
         (UContext.constraints uctx)
     in
     str "incompatible polymorphic binders: got" ++ spc () ++ h 0 (pr_auctx got) ++ spc() ++
     str "but expected" ++ spc() ++ h 0 (pr_auctx expect) ++
     (if not (Int.equal (AUContext.size got) (AUContext.size expect)) then mt() else
-       spc() ++ str "(incompatible constraints)")
+       fnl() ++ str "(incompatible constraints)")
 
 let explain_signature_mismatch l spec why =
   str "Signature components for label " ++ Label.print l ++