From 1bec6b33c62e6b465753ebc17630ea3db433feb1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 17 Dec 2005 22:03:35 +0000
Subject: Création d'un type d'erreur RecursionSchemeError distinct de
 InductiveError (suite)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7662 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/indrec.ml | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index b0dcdde0d7..ef6fccfc40 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -56,7 +56,7 @@ let mis_make_case_com depopt env sigma (ind,mib,mip) kind =
   in
   if not (List.exists ((=) kind) mip.mind_kelim) then
     raise
-      (InductiveError
+      (RecursionSchemeError
 	 (NotAllowedCaseAnalysis
 	    (dep,(new_sort_in_family kind),ind)));
 
@@ -505,11 +505,10 @@ let check_arities listdepkind =
     (fun ln ((_,ni),mibi,mipi,dep,kind) -> 
        let id = mipi.mind_typename  in
        let kelim = mipi.mind_kelim in
-       if not (List.exists ((=) kind) kelim) then
-	 raise
-	   (InductiveError (BadInduction (dep, id, new_sort_in_family kind)))
+       if not (List.exists ((=) kind) kelim) then raise
+	 (RecursionSchemeError (BadInduction (dep,id,new_sort_in_family kind)))
        else if List.mem ni ln then raise
-	   (InductiveError NotMutualInScheme)
+	 (RecursionSchemeError NotMutualInScheme)
        else ni::ln)
 	    [] listdepkind
   in true
@@ -526,7 +525,7 @@ let build_mutual_indrec env sigma = function
                 let (mibi',mipi') = lookup_mind_specif env mind' in
 		(mind',mibi',mipi',dep',s') 
 	      else 
-		raise (InductiveError NotMutualInScheme))
+		raise (RecursionSchemeError NotMutualInScheme))
 	   lrecspec)
       in
       let _ = check_arities listdepkind in 
-- 
cgit v1.2.3