Fixing discriminate for identity.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14157 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 24 insertions, 0 deletions

diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 4fbe361e0..fbf36c1c3 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -46,6 +46,10 @@ let optimize_non_type_induction_scheme kind dep sort ind =
 let build_induction_scheme_in_type dep sort ind =
   build_induction_scheme (Global.env()) Evd.empty ind dep sort
 
+let rect_scheme_kind_from_type =
+  declare_individual_scheme_object "_rect_nodep"
+    (build_induction_scheme_in_type false InType)
+
 let rect_scheme_kind_from_prop =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop"
     (build_induction_scheme_in_type false InType)
@@ -54,6 +58,14 @@ let rect_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_type"
     (build_induction_scheme_in_type true InType)
 
+let rect_dep_scheme_kind_from_prop =
+  declare_individual_scheme_object "_rect_dep"
+    (build_induction_scheme_in_type true InType)
+
+let ind_scheme_kind_from_type =
+  declare_individual_scheme_object "_ind_nodep"
+  (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InProp)
+
 let ind_scheme_kind_from_prop =
   declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop"
   (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InProp)
@@ -62,6 +74,14 @@ let ind_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_ind" ~aux:"_ind_from_type"
   (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InProp)
 
+let ind_dep_scheme_kind_from_prop =
+  declare_individual_scheme_object "_ind_dep"
+  (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_prop true InProp)
+
+let rec_scheme_kind_from_type =
+  declare_individual_scheme_object "_rec_nodep"
+  (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet)
+
 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)
@@ -70,6 +90,10 @@ 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)
 
+let rec_dep_scheme_kind_from_prop =
+  declare_individual_scheme_object "_rec_dep"
+  (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_prop true InSet)
+
 (* Case analysis *)
 
 let build_case_analysis_scheme_in_type dep sort ind =