diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-05-04 19:12:45 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:51:18 +0200 |
| commit | 0c94de1f8c598c1869f71fee86bdbe4f0000a502 (patch) | |
| tree | 766e45ea9bd38c8978542ce90dad3ba1d96b0f98 /printing/printer.ml | |
| parent | 47ce63d23b8efe35babe0f4429c550400afd6b4f (diff) | |
Add printing of cumulativity in inductive types
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index c27a9b009..1d7b7cff0 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -998,6 +998,11 @@ 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_polymorphic b = let print = xor (Flags.is_universe_polymorphism ()) b in if print then |