From 300293c119981054c95182a90c829058530a6b6f Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 25 Dec 2011 13:19:42 +0100
Subject: Imported Upstream version 8.3.pl3

---
 tactics/equality.ml | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

(limited to 'tactics/equality.ml')

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
-- 
cgit v1.2.3