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 /tactics/elimschemes.mli | |
| 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 'tactics/elimschemes.mli')
| -rw-r--r-- | tactics/elimschemes.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli index c36797059..77f927f2d 100644 --- a/tactics/elimschemes.mli +++ b/tactics/elimschemes.mli @@ -13,9 +13,11 @@ open Ind_tables val rect_scheme_kind_from_prop : individual scheme_kind val ind_scheme_kind_from_prop : individual scheme_kind val rec_scheme_kind_from_prop : individual scheme_kind +val rect_scheme_kind_from_type : individual scheme_kind val rect_dep_scheme_kind_from_type : individual scheme_kind val ind_scheme_kind_from_type : individual scheme_kind val ind_dep_scheme_kind_from_type : individual scheme_kind +val rec_scheme_kind_from_type : individual scheme_kind val rec_dep_scheme_kind_from_type : individual scheme_kind |