aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/prettyp.ml7
-rw-r--r--printing/printer.ml43
-rw-r--r--printing/printer.mli6
-rw-r--r--printing/printmod.ml4
-rw-r--r--printing/proof_diffs.ml2
5 files changed, 32 insertions, 30 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..2bbda279bd 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -34,7 +34,7 @@ let should_unfoc() = !enable_unfocused_goal_printing
let should_gname() = !enable_goal_names_printing
-let _ =
+let () =
let open Goptions in
declare_bool_option
{ optdepr = false;
@@ -45,7 +45,7 @@ let _ =
(* This is set on by proofgeneral proof-tree mode. But may be used for
other purposes *)
-let _ =
+let () =
let open Goptions in
declare_bool_option
{ optdepr = false;
@@ -55,7 +55,7 @@ let _ =
optwrite = (fun b -> enable_goal_tags_printing:=b) }
-let _ =
+let () =
let open Goptions in
declare_bool_option
{ optdepr = false;
@@ -140,10 +140,10 @@ let pr_cases_pattern t =
let pr_sort sigma s = pr_glob_sort (extern_sort sigma s)
-let _ = Termops.Internal.set_print_constr
+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()
@@ -430,7 +431,7 @@ let pr_context_limit_compact ?n env sigma =
(* If [None], no limit *)
let print_hyps_limit = ref (None : int option)
-let _ =
+let () =
let open Goptions in
declare_int_option
{ optdepr = false;
@@ -638,7 +639,7 @@ let print_evar_constraints gl sigma =
let should_print_dependent_evars = ref false
-let _ =
+let () =
let open Goptions in
declare_bool_option
{ optdepr = false;
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..a8d7b0c1a8 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -41,7 +41,7 @@ type short = OnlyNames | WithContents
let short = ref false
-let _ =
+let () =
declare_bool_option
{ optdepr = false;
optname = "short module printing";
@@ -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 ->
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index cc1bcc66ae..3e2093db4a 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -52,7 +52,7 @@ let write_diffs_option = function
| "removed" -> diff_option := `REMOVED
| _ -> CErrors.user_err Pp.(str "Diffs option only accepts the following values: \"off\", \"on\", \"removed\".")
-let _ =
+let () =
Goptions.(declare_string_option {
optdepr = false;
optname = "show diffs in proofs";
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 23:54:10 +0000