Fixing discriminate for identity.

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

3 files changed, 36 insertions, 1 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 =
diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli
index a3a8d5edc..06d44550c 100644
--- a/tactics/elimschemes.mli
+++ b/tactics/elimschemes.mli
@@ -14,6 +14,7 @@ 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_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_dep_scheme_kind_from_type : individual scheme_kind
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7dcd58d4e..822198c7c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -676,10 +676,20 @@ let gen_absurdity id gl =
           absurd_term=False
 *)
 
+let ind_scheme_of_eq lbeq =
+  let (mib,mip) = Global.lookup_inductive (destInd lbeq.eq) in
+  let kind = inductive_sort_family mip in
+  (* use ind rather than case by compatibility *)
+  let kind =
+    if kind = InProp then Elimschemes.ind_scheme_kind_from_prop
+    else Elimschemes.ind_scheme_kind_from_type in
+  mkConst (find_scheme kind (destInd lbeq.eq))
+
+
 let discrimination_pf e (t,t1,t2) discriminator lbeq =
   let i           = build_coq_I () in
   let absurd_term = build_coq_False () in
-  let eq_elim     = lbeq.ind in
+  let eq_elim     = ind_scheme_of_eq lbeq in
   (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term)
 
 exception NotDiscriminable