diff options
| author | Amin Timany | 2017-06-01 16:18:19 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-06-16 04:51:19 +0200 |
| commit | ff918e4bb0ae23566e038f4b55d84dd2c343f95e (patch) | |
| tree | ebab76cc4dedaf307f96088a3756d8292a341433 /printing/printer.ml | |
| parent | 3380f47d2bb38d549fcdac8fb073f9aa1f259a23 (diff) | |
Clean up universes of constants and inductives
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 1d7b7cff0f..3b0b6d5d23 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -261,10 +261,11 @@ let pr_universe_ctx sigma c = else mt() -let pr_universe_info_ind sigma uii = - if !Detyping.print_universes && not (Univ.UInfoInd.is_empty uii) then - fnl()++pr_in_comment (fun uii -> v 0 - (Univ.pr_universe_info_ind (Termops.pr_evd_level sigma) uii)) uii +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() @@ -998,10 +999,10 @@ let pr_assumptionset env s = let xor a b = (a && not b) || (not a && b) -let pr_cumulative p b = - if p then - if b then str "Cumulative " else str "NonCumulative " - else str "" +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 |