Création d'un type d'erreur RecursionSchemeError distinct de InductiveError et suite correction bug #1028

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7660 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 29 insertions, 12 deletions

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 0325a3acd..b0dcdde0d 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -23,11 +23,18 @@ open Environ
 open Reductionops
 open Typeops
 open Type_errors
-open Indtypes (* pour les erreurs *)
 open Safe_typing
 open Nametab
 open Sign
 
+(* Errors related to recursors building *)
+type recursion_scheme_error =
+  | NotAllowedCaseAnalysis of bool * sorts * inductive
+  | BadInduction of bool * identifier * sorts
+  | NotMutualInScheme
+
+exception RecursionSchemeError of recursion_scheme_error
+
 let make_prod_dep dep env = if dep then prod_name env else mkProd
 let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c)
 
@@ -442,7 +449,7 @@ let make_case_gen env   = make_case_com None env
 
 
 (**********************************************************************)
-(* [instanciate_indrec_scheme s rec] replace the sort of the scheme
+(* [instantiate_indrec_scheme s rec] replace the sort of the scheme
    [rec] by [s] *)
 
 let change_sort_arity sort = 
@@ -456,7 +463,7 @@ let change_sort_arity sort =
   drec 
 
 (* [npar] is the number of expected arguments (then excluding letin's) *)
-let instanciate_indrec_scheme sort =
+let instantiate_indrec_scheme sort =
   let rec drec npar elim =
     match kind_of_term elim with
       | Lambda (n,t,c) -> 
@@ -465,13 +472,13 @@ let instanciate_indrec_scheme sort =
 	  else 
 	    mkLambda (n, t, drec (npar-1) c)
       | LetIn (n,b,t,c) -> mkLetIn (n,b,t,drec npar c)
-      | _ -> anomaly "instanciate_indrec_scheme: wrong elimination type"
+      | _ -> anomaly "instantiate_indrec_scheme: wrong elimination type"
   in
   drec
 
 (* Change the sort in the type of an inductive definition, builds the
    corresponding eta-expanded term *)
-let instanciate_type_indrec_scheme sort npars term =
+let instantiate_type_indrec_scheme sort npars term =
   let rec drec np elim =
     match kind_of_term elim with
       | Prod (n,t,c) -> 
@@ -484,7 +491,7 @@ let instanciate_type_indrec_scheme sort npars term =
 	    mkProd (n, t, c'), mkLambda (n, t, term')
       | LetIn (n,b,t,c) -> let c',term' = drec np c in
            mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term') 
-      | _ -> anomaly "instanciate_type_indrec_scheme: wrong elimination type"
+      | _ -> anomaly "instantiate_type_indrec_scheme: wrong elimination type"
   in
   drec npars
 
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index 2306201b2..f0f7747cb 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -17,7 +17,16 @@ open Environ
 open Evd
 (*i*)
 
-(* Eliminations. *)
+(* Errors related to recursors building *)
+
+type recursion_scheme_error =
+  | NotAllowedCaseAnalysis of bool * sorts * inductive
+  | BadInduction of bool * identifier * sorts
+  | NotMutualInScheme
+
+exception RecursionSchemeError of recursion_scheme_error
+
+(** Eliminations *)
 
 (* These functions build elimination predicate for Case tactic *)
 
@@ -29,11 +38,11 @@ val make_case_gen : env -> evar_map -> inductive -> sorts_family -> constr
    of the inductive) *)
 
 val build_indrec : env -> evar_map -> inductive -> constr
-val instanciate_indrec_scheme : sorts -> int -> constr -> constr
-val instanciate_type_indrec_scheme : sorts -> int -> constr -> types ->
+val instantiate_indrec_scheme : sorts -> int -> constr -> constr
+val instantiate_type_indrec_scheme : sorts -> int -> constr -> types ->
   constr * types
 
-(* This builds complex [Scheme] *)
+(** Complex recursion schemes [Scheme] *)
 
 val build_mutual_indrec : 
   env -> evar_map ->
@@ -41,7 +50,7 @@ val build_mutual_indrec :
     * bool * sorts_family) list
     -> constr list
 
-(* These are for old Case/Match typing *)
+(** Old Case/Match typing *)
 
 val type_rec_branches : bool -> env -> evar_map -> inductive_type
   -> constr -> constr -> constr array * constr
@@ -50,7 +59,8 @@ val make_rec_branch_arg :
     int * ('b * constr) option array * int ->
     constr -> constructor_summary -> wf_paths list -> constr
 
-(* *)
+(** Recursor names utilities *)
+
 val lookup_eliminator : inductive -> sorts_family -> constr
 val elimination_suffix : sorts_family -> string
 val make_elimination_ident : identifier -> sorts_family -> identifier