diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-15 21:01:57 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-24 19:18:56 +0100 |
| commit | a5feb9687819c5e7ef0db6e7b74d0e236a296674 (patch) | |
| tree | bfd809fd50c8db88f390e3d5cba22360a0c90724 /printing | |
| parent | d437078a4ca82f7ca6d19be5ee9452359724f9a0 (diff) | |
Separate checking univ_decls and obtaining universe binder names.
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 d7bb0460d..4d5cfcba3 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 e014baa2c..a3d0eaac2 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 *) |