aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.ml
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-05-26 10:54:02 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-05-26 10:54:02 +0000
commitd4a2d6a80b57485467d6141f1140c2aee577495f (patch)
treecdc612c148d70d419525786dcf0ecc92508fa592 /tactics/equality.ml
parent7f19da0503ce5895f3ad4080f4fb96dc2287aa26 (diff)
Fixing discriminate for identity.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14157 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/equality.ml')
-rw-r--r--tactics/equality.ml12
1 files changed, 11 insertions, 1 deletions
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