Local universes for opaque polymorphic constants.

4 files changed, 18 insertions, 12 deletions

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 712eb21ee6..f9f4d7f7f8 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -96,8 +96,9 @@ let print_ref reduce ref udecl =
     then Printer.pr_universe_instance sigma inst
     else mt ()
   in
+  let priv = None in (* We deliberately don't print private univs in About. *)
   hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ 
-           Printer.pr_abstract_universe_ctx sigma ?variance univs)
+           Printer.pr_abstract_universe_ctx sigma ?variance univs ~priv)
 
 (********************************)
 (** Printing implicit arguments *)
@@ -580,11 +581,11 @@ let print_constant with_values sep sp udecl =
 	str"*** [ " ++
 	print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++
 	str" ]" ++
-        Printer.pr_constant_universes sigma univs
+        Printer.pr_constant_universes sigma univs ~priv:cb.const_private_poly_univs
     | Some (c, ctx) ->
 	print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++
 	(if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++
-        Printer.pr_constant_universes sigma univs)
+        Printer.pr_constant_universes sigma univs ~priv:cb.const_private_poly_univs)
 
 let gallina_print_constant_with_infos sp udecl =
   print_constant true " = " sp udecl ++
diff --git a/printing/printer.ml b/printing/printer.ml
index 4840577cbf..ebe8e3eebb 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -211,16 +211,21 @@ let pr_universe_ctx sigma ?variance c =
   else
     mt()
 
-let pr_abstract_universe_ctx sigma ?variance c =
-  if !Detyping.print_universes && not (Univ.AUContext.is_empty c) then
+let pr_abstract_universe_ctx sigma ?variance c ~priv =
+  let open Univ in
+  let priv = Option.default Univ.ContextSet.empty priv in
+  if !Detyping.print_universes && not (Univ.AUContext.is_empty c && Univ.ContextSet.is_empty priv) then
+    let local = if ContextSet.is_empty priv then mt() else
+        str "local: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) priv
+    in
     fnl()++pr_in_comment (fun c -> v 0
-      (Univ.pr_abstract_universe_context (Termops.pr_evd_level sigma) ?variance c)) c
+      (Univ.pr_abstract_universe_context (Termops.pr_evd_level sigma) ?variance c) ++ v 0 local) c
   else
     mt()
 
-let pr_constant_universes sigma = function
+let pr_constant_universes sigma ~priv = function
   | Declarations.Monomorphic_const ctx -> pr_universe_ctx_set sigma ctx
-  | Declarations.Polymorphic_const ctx -> pr_abstract_universe_ctx sigma ctx
+  | Declarations.Polymorphic_const ctx -> pr_abstract_universe_ctx sigma ctx ~priv
 
 let pr_cumulativity_info sigma cumi =
   if !Detyping.print_universes 
diff --git a/printing/printer.mli b/printing/printer.mli
index cefc005c74..b0232ec4ac 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -87,10 +87,10 @@ 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 ->
-  Univ.AUContext.t -> Pp.t
+val pr_abstract_universe_ctx : evar_map -> ?variance:Univ.Variance.t array ->
+  Univ.AUContext.t -> priv:Univ.ContextSet.t option -> Pp.t
 val pr_universe_ctx_set    : evar_map -> Univ.ContextSet.t -> Pp.t
-val pr_constant_universes  : evar_map -> Declarations.constant_universes -> Pp.t
+val pr_constant_universes  : evar_map -> priv:Univ.ContextSet.t option -> Declarations.constant_universes -> Pp.t
 val pr_cumulativity_info   : evar_map -> Univ.CumulativityInfo.t -> Pp.t
 val pr_abstract_cumulativity_info   : evar_map -> Univ.ACumulativityInfo.t -> Pp.t
 
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 2c3ab46670..1360ad4af4 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -310,7 +310,7 @@ let print_body is_impl extent env mp (l,body) =
 		hov 2 (str ":= " ++
                        Printer.pr_lconstr_env env sigma (Mod_subst.force_constr l))
 	      | _ -> mt ()) ++ str "." ++
-            Printer.pr_abstract_universe_ctx sigma ctx)
+            Printer.pr_abstract_universe_ctx sigma ctx ~priv:cb.const_private_poly_univs)
     | SFBmind mib ->
       match extent with
       | WithContents ->