The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi Vladimir,

> I wonder if there is an easy way to make discriminate work with [
> identity ] instead of [ eq ] ?

It used to work at some time and it now reworks in v8.3 branch. A
patch is also attached. Note that it works for
Coq.Init.Logic_type.identity only (not for a redefinition of it).

Hugo
diff --git a/branches/v8.3/interp/coqlib.ml b/branches/v8.3/interp/coqlib.ml
index b91547c..ab1cf25 100644
--- a/branches/v8.3/interp/coqlib.ml
+++ b/branches/v8.3/interp/coqlib.ml
@@ -298,7 +298,7 @@ let build_coq_sumbool () = Lazy.force coq_sumbool
 
 (* Equality on Type as a Type *)
 let coq_identity_eq = lazy_init_constant ["Datatypes"] "identity"
-let coq_identity_refl = lazy_init_constant ["Datatypes"] "refl_identity"
+let coq_identity_refl = lazy_init_constant ["Datatypes"] "identity_refl"
 let coq_identity_ind = lazy_init_constant ["Datatypes"] "identity_ind"
 let coq_identity_rec = lazy_init_constant ["Datatypes"] "identity_rec"
 let coq_identity_rect = lazy_init_constant ["Datatypes"] "identity_rect"
diff --git a/branches/v8.3/tactics/elimschemes.mli 
b/branches/v8.3/tactics/elimschemes.mli
index 795add1..6d38018 100644
--- a/branches/v8.3/tactics/elimschemes.mli
+++ b/branches/v8.3/tactics/elimschemes.mli
@@ -16,6 +16,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/branches/v8.3/tactics/equality.ml 
b/branches/v8.3/tactics/equality.ml
index 4f9354a..201632b 100644
--- a/branches/v8.3/tactics/equality.ml
+++ b/branches/v8.3/tactics/equality.ml
@@ -681,10 +681,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