diff options
| author | Matthieu Sozeau | 2016-05-24 20:32:35 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-07-06 14:38:04 +0200 |
| commit | a9010048c40c85b0f5e9c5fedaf2609121e71b89 (patch) | |
| tree | 3aa6bf4ab94a56f547424cfe527cf53e4404f8cc /tactics | |
| 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')
| -rw-r--r-- | tactics/elimschemes.ml | 4 | ||||
| -rw-r--r-- | tactics/elimschemes.mli | 2 |
2 files changed, 6 insertions, 0 deletions
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index de28189023..99c2d82106 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -95,6 +95,10 @@ let rec_scheme_kind_from_prop = declare_individual_scheme_object "_rec" ~aux:"_rec_from_prop" (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InSet) +let rec_scheme_kind_from_type = + declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type" + (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet) + let rec_dep_scheme_kind_from_type = declare_individual_scheme_object "_rec" ~aux:"_rec_from_type" (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InSet) diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli index c36797059e..77f927f2df 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 |