diff options
| author | Pierre-Marie Pédrot | 2015-07-09 14:50:16 +0900 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-07-09 14:53:39 +0900 |
| commit | 7bda7d7070fc55fc38fef4c21557ea61b0c4d17d (patch) | |
| tree | 6aed32be2e6a2debd748af2d8e7c0838aa40cbe0 | |
| parent | a198b3f7402d4b275a7fc67ece827843f00dadf0 (diff) | |
Fixing printing of primitive coinductive record status.
They do not have eta-rule indeed, even though it was displayed as such.
| -rw-r--r-- | printing/prettyp.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index e50435cda2..b8c5fd4cfc 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -205,16 +205,20 @@ let print_polymorphism ref = else "not universe polymorphic") ] else [] -let print_primitive_record mipv = function +let print_primitive_record recflag mipv = function | Some (Some (_, ps,_)) -> - [pr_id mipv.(0).mind_typename ++ str" is primitive and has eta conversion."] + let eta = match recflag with + | Decl_kinds.CoFinite -> mt () + | Decl_kinds.Finite | Decl_kinds.BiFinite -> str " and has eta conversion" + in + [pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."] | _ -> [] 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 + print_primitive_record mib.mind_finite mib.mind_packets mib.mind_record | _ -> [] let print_name_infos ref = @@ -447,7 +451,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 mib.mind_finite mipv mib.mind_record @ print_inductive_renames sp mipv @ print_inductive_implicit_args sp mipv @ print_inductive_argument_scopes sp mipv) |