diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-29 00:24:13 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-29 00:24:13 +0200 |
| commit | 791a0c87624c394bd2c4dcb37a73bd04aafa5e98 (patch) | |
| tree | 79f69b548488a61f88daecb342a80e4abe251bdb /printing/prettyp.ml | |
| parent | 6e22ae3f21ae32f298b6e3463448f59a5c7d1f76 (diff) | |
Fix printing of primitive record info.
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 8b68c6274..08d7c237d 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -206,15 +206,15 @@ let print_polymorphism ref = let print_primitive_record mipv = function | Some (ps,_) when Array.length ps > 0 -> - pr_id mipv.(0).mind_typename ++ str" is primitive and has eta conversion." - | _ -> mt() - + [pr_id mipv.(0).mind_typename ++ str" is primitive and has eta conversion."] + | _ -> [] + let print_primitive ref = match ref with | IndRef ind -> let mib,_ = Global.lookup_inductive ind in print_primitive_record mib.mind_packets mib.mind_record - | _ -> mt() + | _ -> [] let print_name_infos ref = let poly = print_polymorphism ref in @@ -229,7 +229,7 @@ let print_name_infos ref = print_ref true ref; blankline] else [] in - poly :: print_primitive ref :: + poly :: print_primitive ref @ type_info_for_implicit @ print_renames_list (mt()) renames @ print_impargs_list (mt()) impls @ @@ -446,7 +446,7 @@ let gallina_print_inductive sp = let mipv = mib.mind_packets in pr_mutual_inductive_body env sp mib ++ with_line_skip - (print_primitive_record mipv mib.mind_record :: + (print_primitive_record mipv mib.mind_record @ print_inductive_renames sp mipv @ print_inductive_implicit_args sp mipv @ print_inductive_argument_scopes sp mipv) |