diff options
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index d6f0778f75..3b0b6d5d23 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -261,6 +261,14 @@ let pr_universe_ctx sigma c = else mt() +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 + else + mt() + (**********************************************************************) (* Global references *) @@ -991,6 +999,11 @@ let pr_assumptionset env s = let xor a b = (a && not b) || (not a && b) +let pr_cumulative poly cum = + if poly then + if cum then str "Cumulative " else str "NonCumulative " + else mt () + let pr_polymorphic b = let print = xor (Flags.is_universe_polymorphism ()) b in if print then |