From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 1 Feb 2009 00:54:40 +0100
Subject: Imported Upstream version 8.2~rc2+dfsg

---
 pretyping/indrec.ml | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

(limited to 'pretyping/indrec.ml')

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index b4b8f0b8..d3123eb6 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: indrec.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: indrec.ml 11735 2009-01-02 17:22:31Z herbelin $ *)
 
 open Pp
 open Util
@@ -29,8 +29,7 @@ open Sign
 
 (* Errors related to recursors building *)
 type recursion_scheme_error =
-  | NotAllowedCaseAnalysis of bool * sorts * inductive
-  | BadInduction of bool * identifier * sorts
+  | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * inductive
   | NotMutualInScheme of inductive * inductive
 
 exception RecursionSchemeError of recursion_scheme_error
@@ -57,8 +56,7 @@ let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind =
   if not (List.mem kind (elim_sorts specif)) then
     raise
       (RecursionSchemeError
-	 (NotAllowedCaseAnalysis
-	    (dep,(new_sort_in_family kind),ind)));
+	 (NotAllowedCaseAnalysis (false,new_sort_in_family kind,ind)));
 
   let ndepar = mip.mind_nrealargs + 1 in
 
@@ -502,10 +500,10 @@ let instantiate_type_indrec_scheme sort npars term =
 let check_arities listdepkind = 
   let _ = List.fold_left
     (fun ln ((_,ni as mind),mibi,mipi,dep,kind) -> 
-       let id = mipi.mind_typename  in
        let kelim = elim_sorts (mibi,mipi) in
        if not (List.exists ((=) kind) kelim) then raise
-	 (RecursionSchemeError (BadInduction (dep,id,new_sort_in_family kind)))
+	 (RecursionSchemeError
+	   (NotAllowedCaseAnalysis (true,new_sort_in_family kind,mind)))
        else if List.mem ni ln then raise
 	 (RecursionSchemeError (NotMutualInScheme (mind,mind)))
        else ni::ln)
@@ -593,7 +591,8 @@ let lookup_eliminator ind_sp s =
     errorlabstrm "default_elim"
       (strbrk "Cannot find the elimination combinator " ++
        pr_id id ++ strbrk ", the elimination of the inductive definition " ++
-       pr_id id ++ strbrk " on sort " ++ pr_sort_family s ++
+       pr_global_env Idset.empty (IndRef ind_sp) ++ 
+       strbrk " on sort " ++ pr_sort_family s ++
        strbrk " is probably not allowed.")
 
 
-- 
cgit v1.2.3