diff options
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 de2818902..99c2d8210 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) |