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/printmod.ml | |
| parent | 47ce63d23b8efe35babe0f4429c550400afd6b4f (diff) | |
Add printing of cumulativity in inductive types
Diffstat (limited to 'printing/printmod.ml')
| -rw-r--r-- | printing/printmod.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml index 7dc47a4a4..be8940b6f 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -121,10 +121,11 @@ let print_mutual_inductive env mind mib = let bl = Universes.universe_binders_of_global (IndRef (mind, 0)) in let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in hov 0 (Printer.pr_polymorphic mib.mind_polymorphic ++ - def keyword ++ spc () ++ - prlist_with_sep (fun () -> fnl () ++ str" with ") - (print_one_inductive env sigma mib) inds ++ - Printer.pr_universe_info_ind sigma (Univ.instantiate_univ_info_ind mib.mind_universes)) + Printer.pr_cumulative mib.mind_polymorphic mib.mind_cumulative ++ + def keyword ++ spc () ++ + prlist_with_sep (fun () -> fnl () ++ str" with ") + (print_one_inductive env sigma mib) inds ++ + Printer.pr_universe_info_ind sigma (Univ.instantiate_univ_info_ind mib.mind_universes)) let get_fields = let rec prodec_rec l subst c = @@ -165,6 +166,7 @@ let print_record env mind mib = hov 0 ( hov 0 ( Printer.pr_polymorphic mib.mind_polymorphic ++ + Printer.pr_cumulative mib.mind_polymorphic mib.mind_cumulative ++ def keyword ++ spc () ++ pr_id mip.mind_typename ++ brk(1,4) ++ print_params env sigma params ++ str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++ |