diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-20 00:12:09 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-20 00:12:09 +0100 |
| commit | be3a07eafa86a23f06297a9f971413ecfbe41959 (patch) | |
| tree | e9081ea7badfa0ba4264511def74b758f61871ed /printing/printmod.ml | |
| parent | 3d5936f280bc01bd6baa8b4396e641ac156bfd5b (diff) | |
Setting printing flags on the printing of mutual inductives.
Diffstat (limited to 'printing/printmod.ml')
| -rw-r--r-- | printing/printmod.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml index e19b3a92d..84d4208f9 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -105,12 +105,12 @@ let print_mutual_inductive env mind mib = let keyword = let open Decl_kinds in match mib.mind_finite with - | Finite -> "Inductive " - | BiFinite -> "Variant " - | CoFinite -> "CoInductive " + | Finite -> "Inductive" + | BiFinite -> "Variant" + | CoFinite -> "CoInductive" in hov 0 (Printer.pr_polymorphic mib.mind_polymorphic ++ - str keyword ++ + def keyword ++ spc () ++ prlist_with_sep (fun () -> fnl () ++ str" with ") (print_one_inductive env mib) inds ++ Printer.pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes)) @@ -145,14 +145,14 @@ let print_record env mind mib = let keyword = let open Decl_kinds in match mib.mind_finite with - | BiFinite -> "Record " - | Finite -> "Inductive " - | CoFinite -> "CoInductive " + | BiFinite -> "Record" + | Finite -> "Inductive" + | CoFinite -> "CoInductive" in hov 0 ( hov 0 ( Printer.pr_polymorphic mib.mind_polymorphic ++ - str keyword ++ pr_id mip.mind_typename ++ brk(1,4) ++ + def keyword ++ spc () ++ pr_id mip.mind_typename ++ brk(1,4) ++ print_params env Evd.empty params ++ str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ brk(1,2) ++ str ":= " ++ pr_id mip.mind_consnames.(0)) ++ |