diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/printer.ml | 7 | ||||
| -rw-r--r-- | printing/printer.mli | 1 |
2 files changed, 8 insertions, 0 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index d7bb0460d5..4d5cfcba32 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -256,6 +256,13 @@ let safe_pr_constr t = let (sigma, env) = Pfedit.get_current_context () in safe_pr_constr_env env sigma t +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 + else + mt() + let pr_universe_ctx sigma c = if !Detyping.print_universes && not (Univ.UContext.is_empty c) then fnl()++pr_in_comment (fun c -> v 0 diff --git a/printing/printer.mli b/printing/printer.mli index e014baa2cd..a3d0eaac2e 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -121,6 +121,7 @@ val pr_polymorphic : bool -> Pp.t val pr_cumulative : bool -> bool -> Pp.t val pr_universe_instance : evar_map -> Univ.UContext.t -> Pp.t val pr_universe_ctx : evar_map -> Univ.UContext.t -> Pp.t +val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t (** Printing global references using names as short as possible *) |