diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-03 15:52:12 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-04 10:25:55 +0200 |
| commit | a93dbac35ed828286b0af9e5c6597081ed24a553 (patch) | |
| tree | 7e25dc399c171fa246d72411847912c0797932df | |
| parent | af0dad8ef026943b31025c5b4a7a552c19b7fdfa (diff) | |
Inductive and CoInductive records are printed correctly.
| -rw-r--r-- | printing/printer.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 7971e0aaa..8c7dbac33 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -820,10 +820,17 @@ let print_record env mind mib = let cstrtype = hnf_prod_applist env cstrtypes.(0) args in let fields = get_fields cstrtype in let envpar = push_rel_context params env in + let keyword = + let open Decl_kinds in + match mib.mind_finite with + | BiFinite -> "Record " + | Finite -> "Inductive " + | CoFinite -> "CoInductive " + in hov 0 ( hov 0 ( pr_polymorphic mib.mind_polymorphic ++ - str "Record " ++ pr_id mip.mind_typename ++ brk(1,4) ++ + str keyword ++ pr_id mip.mind_typename ++ brk(1,4) ++ print_params env params ++ str ": " ++ pr_lconstr_env envpar arity ++ brk(1,2) ++ str ":= " ++ pr_id mip.mind_consnames.(0)) ++ |