From c35f5d4f93e4eca1b704722bd3c207783e97649a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 17 May 2007 18:55:42 +0000
Subject: Nettoyage et standardisation des messages d'erreurs.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9831 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/indrec.ml  | 8 ++++----
 pretyping/indrec.mli | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 7fd65050c5..84f35241ab 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -31,7 +31,7 @@ open Sign
 type recursion_scheme_error =
   | NotAllowedCaseAnalysis of bool * sorts * inductive
   | BadInduction of bool * identifier * sorts
-  | NotMutualInScheme
+  | NotMutualInScheme of inductive * inductive
 
 exception RecursionSchemeError of recursion_scheme_error
 
@@ -501,13 +501,13 @@ let instantiate_type_indrec_scheme sort npars term =
 
 let check_arities listdepkind = 
   let _ = List.fold_left
-    (fun ln ((_,ni),mibi,mipi,dep,kind) -> 
+    (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)))
        else if List.mem ni ln then raise
-	 (RecursionSchemeError NotMutualInScheme)
+	 (RecursionSchemeError (NotMutualInScheme (mind,mind)))
        else ni::ln)
 	    [] listdepkind
   in true
@@ -524,7 +524,7 @@ let build_mutual_indrec env sigma = function
                 let (mibi',mipi') = lookup_mind_specif env mind' in
 		(mind',mibi',mipi',dep',s') 
 	      else 
-		raise (RecursionSchemeError NotMutualInScheme))
+		raise (RecursionSchemeError (NotMutualInScheme (mind,mind'))))
 	   lrecspec)
       in
       let _ = check_arities listdepkind in 
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index f0f7747cb6..b172935f58 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -22,7 +22,7 @@ open Evd
 type recursion_scheme_error =
   | NotAllowedCaseAnalysis of bool * sorts * inductive
   | BadInduction of bool * identifier * sorts
-  | NotMutualInScheme
+  | NotMutualInScheme of inductive * inductive
 
 exception RecursionSchemeError of recursion_scheme_error
 
-- 
cgit v1.2.3