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/elimschemes.ml | |
| 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.ml')
| -rw-r--r-- | tactics/elimschemes.ml | 4 |
1 files changed, 4 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) |