Merge PR #8894: Print full binders in subtyping incompatible polymorphism error.

4 files changed, 25 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 da364c8b9e..7ce08ed6bc 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -244,8 +244,19 @@ let pr_abstract_cumulativity_info sigma cumi =
 let pr_global_env = Nametab.pr_global_env
 let pr_global = pr_global_env Id.Set.empty
 
+let pr_universe_instance_constraints evd inst csts =
+  let open Univ in
+  let prlev = Termops.pr_evd_level evd in
+  let pcsts = if Constraint.is_empty csts then mt()
+    else str " |= " ++
+         prlist_with_sep (fun () -> str "," ++ spc())
+           (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"}"
+
 let pr_universe_instance evd inst =
-  str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}"
+  pr_universe_instance_constraints evd inst Univ.Constraint.empty
 
 let pr_puniverses f env sigma (c,u) =
   if !Constrextern.print_universes
diff --git a/printing/printer.mli b/printing/printer.mli
index f9d1a62895..e50b02b508 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -85,6 +85,7 @@ val pr_sort                : evar_map -> Sorts.t -> Pp.t
 val pr_polymorphic         : bool -> Pp.t
 val pr_cumulative          : bool -> bool -> Pp.t
 val pr_universe_instance   : evar_map -> Univ.Instance.t -> Pp.t
+val pr_universe_instance_constraints : evar_map -> Univ.Instance.t -> Univ.Constraint.t -> Pp.t
 val pr_universe_ctx        : evar_map -> ?variance:Univ.Variance.t array ->
   Univ.UContext.t -> Pp.t
 val pr_abstract_universe_ctx        : evar_map -> ?variance:Univ.Variance.t array ->
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) ++