Merge PR #8850: Private universes for opaque polymorphic constants.

4 files changed, 24 insertions, 22 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..94b514239a 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -143,7 +143,7 @@ let pr_sort sigma s = pr_glob_sort (extern_sort sigma s)
 let _ = Termops.Internal.set_print_constr
   (fun env sigma t -> pr_lconstr_expr (extern_constr ~lax:true false env sigma t))
 
-let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
+let pr_in_comment x = str "(* " ++ x ++ str " *)"
 
 (** Term printers resilient to [Nametab] errors *)
 
@@ -199,42 +199,43 @@ let safe_pr_constr_env = safe_gen pr_constr_env
 
 let pr_universe_ctx_set sigma c =
   if !Detyping.print_universes && not (Univ.ContextSet.is_empty c) then
-    fnl()++pr_in_comment (fun c -> v 0
-      (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c)) c
+    fnl()++pr_in_comment (v 0 (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c))
   else
     mt()
 
 let pr_universe_ctx sigma ?variance c =
   if !Detyping.print_universes && not (Univ.UContext.is_empty c) then
-    fnl()++pr_in_comment (fun c -> v 0 
-      (Univ.pr_universe_context (Termops.pr_evd_level sigma) ?variance c)) c
+    fnl()++pr_in_comment (v 0 (Univ.pr_universe_context (Termops.pr_evd_level sigma) ?variance c))
   else
     mt()
 
-let pr_abstract_universe_ctx sigma ?variance c =
-  if !Detyping.print_universes && not (Univ.AUContext.is_empty c) then
-    fnl()++pr_in_comment (fun c -> v 0
-      (Univ.pr_abstract_universe_context (Termops.pr_evd_level sigma) ?variance c)) c
+let pr_abstract_universe_ctx sigma ?variance c ~priv =
+  let open Univ in
+  let priv = Option.default Univ.ContextSet.empty priv in
+  let has_priv = not (ContextSet.is_empty priv) in
+  if !Detyping.print_universes && (not (Univ.AUContext.is_empty c) || has_priv) then
+    let prlev u = Termops.pr_evd_level sigma u in
+    let pub = (if has_priv then str "Public universes:" ++ fnl() else mt()) ++ v 0 (Univ.pr_abstract_universe_context prlev ?variance c) in
+    let priv = if has_priv then fnl() ++ str "Private universes:" ++ fnl() ++ v 0 (Univ.pr_universe_context_set prlev priv) else mt() in
+    fnl()++pr_in_comment (pub ++ priv)
   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 
   && not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then
-    fnl()++pr_in_comment (fun uii -> v 0 
-      (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi
+    fnl()++pr_in_comment (v 0 (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) cumi))
   else
     mt()
 
 let pr_abstract_cumulativity_info sigma cumi =
   if !Detyping.print_universes
   && not (Univ.AUContext.is_empty (Univ.ACumulativityInfo.univ_context cumi)) then
-    fnl()++pr_in_comment (fun uii -> v 0
-      (Univ.pr_abstract_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi
+    fnl()++pr_in_comment (v 0 (Univ.pr_abstract_cumulativity_info (Termops.pr_evd_level sigma) cumi))
   else
     mt()
 
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 ->