diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-05-24 20:32:35 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-07-06 14:38:04 +0200 |
| commit | a9010048c40c85b0f5e9c5fedaf2609121e71b89 (patch) | |
| tree | 3aa6bf4ab94a56f547424cfe527cf53e4404f8cc /printing | |
| parent | 9a1eb2f4fefcc52f56785f20831e854bb626ae95 (diff) | |
primproj: warning and avoid error.
When defining a (co)recursive inductive with primitive projections on,
which lacks eta-conversion and hence dependent elimination, build only
the associated non-dependent elimination principles, and warn about
this. Also make the printing of the status of an inductive
w.r.t. projections and eta conversion explicit in Print and About.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/prettyp.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 1f6e99c7e..f71719cb9 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -224,12 +224,12 @@ let print_type_in_type ref = let print_primitive_record recflag mipv = function | Some (Some (_, ps,_)) -> let eta = match recflag with - | Decl_kinds.CoFinite | Decl_kinds.Finite -> mt () - | Decl_kinds.BiFinite -> str " and has eta conversion" + | Decl_kinds.CoFinite | Decl_kinds.Finite -> str" without eta conversion" + | Decl_kinds.BiFinite -> str " with eta conversion" in - [pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."] + [pr_id mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."] | _ -> [] - + let print_primitive ref = match ref with | IndRef ind -> |