diff options
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 411ccc0e..a25f88e3 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: equality.ml 13874 2011-03-05 16:41:53Z herbelin $ *) +(* $Id: equality.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util @@ -681,10 +681,21 @@ let gen_absurdity id gl = absurd_term=False *) +let ind_scheme_of_eq lbeq = + let ind = destInd lbeq.eq in + let (mib,mip) = Global.lookup_inductive ind 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 ind) + + 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 |