diff options
| author | Matthieu Sozeau | 2014-09-28 11:46:54 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-28 11:46:54 +0200 |
| commit | 199bb343f7e4367d843ab5ae76ba9a4de89eddbc (patch) | |
| tree | 69e91f73c75a5a6d8d7020c3a0153aa372b473eb | |
| parent | 3fe4912b568916676644baeb982a3e10c592d887 (diff) | |
Print information about primitive records (Print and About).
| -rw-r--r-- | printing/prettyp.ml | 19 |
1 files changed, 16 insertions, 3 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index b084c0dd1c..8b68c62743 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -203,7 +203,19 @@ let print_polymorphism ref = else if template_poly then "template universe polymorphic" else "not universe polymorphic") - + +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() + +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 let impls = implicits_of_global ref in @@ -217,7 +229,7 @@ let print_name_infos ref = print_ref true ref; blankline] else [] in - poly :: + poly :: print_primitive ref :: type_info_for_implicit @ print_renames_list (mt()) renames @ print_impargs_list (mt()) impls @ @@ -434,7 +446,8 @@ let gallina_print_inductive sp = let mipv = mib.mind_packets in pr_mutual_inductive_body env sp mib ++ with_line_skip - (print_inductive_renames sp mipv @ + (print_primitive_record mipv mib.mind_record :: + print_inductive_renames sp mipv @ print_inductive_implicit_args sp mipv @ print_inductive_argument_scopes sp mipv) |