Ajouts des causes d'erreur de Indrec

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

4 files changed, 17 insertions, 5 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index e48e9dc97..9335a63b7 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -5,6 +5,7 @@ open Util
 open Names
 open Generic
 open Term
+open Constant
 open Inductive
 open Sign
 open Environ
@@ -25,6 +26,7 @@ open Typeops
 (* Various well-formedness check for inductive declarations            *)
 
 type inductive_error =
+  (* These are errors related to inductive constructions in this module *)
   | NonPos of name list * constr * constr
   | NotEnoughArgs of name list * constr * constr
   | NotConstructor of name list * constr * constr
@@ -33,6 +35,10 @@ type inductive_error =
   | SameNamesConstructors of identifier * identifier
   | NotAnArity of identifier
   | BadEntry
+  (* These are errors related to recursors building in Indrec *)
+  | NotAllowedCaseAnalysis of bool * sorts * inductive
+  | BadInduction of bool * identifier * sorts
+  | NotMutualInScheme
 
 exception InductiveError of inductive_error
 
@@ -225,7 +231,7 @@ let listrec_mconstr env ntypes nparams i indlc =
       (* when substituted *) 
       Array.map 
 	(function c -> 
-	   let c' = hnf_prod_appvect env Evd.empty "is_imbr_pos" c 
+	   let c' = hnf_prod_appvect env Evd.empty c 
 		      (Array.map (lift auxntyp) lpar) in 
 	   check_construct false newidx c') 
 	auxlcvect
@@ -312,6 +318,7 @@ let cci_inductive env env_ar kind nparams finite inds cst =
       mind_lc = lc;
       mind_nrealargs = List.length ar_sign - nparams;
       mind_arity  = ar;
+      mind_sort = ar_sort;
       mind_kelim = kelim;
       mind_listrec = recargs;
       mind_finite = finite }
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index e955f6009..505ea1d95 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -5,7 +5,7 @@
 open Names
 open Univ
 open Term
-open Inductive
+open Constant
 open Environ
 (*i*)
 
@@ -14,6 +14,7 @@ open Environ
   definition. *)
 
 type inductive_error =
+  (* These are errors related to inductive constructions in this module *)
   | NonPos of name list * constr * constr
   | NotEnoughArgs of name list * constr * constr
   | NotConstructor of name list * constr * constr
@@ -22,6 +23,10 @@ type inductive_error =
   | SameNamesConstructors of identifier * identifier
   | NotAnArity of identifier
   | BadEntry
+  (* These are errors related to recursors building in Indrec *)
+  | NotAllowedCaseAnalysis of bool * sorts * inductive
+  | BadInduction of bool * identifier * sorts
+  | NotMutualInScheme
 
 exception InductiveError of inductive_error
 
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 3cca1c694..8ca7135aa 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -15,7 +15,7 @@ type type_error =
   | NotAType of constr
   | BadAssumption of constr
   | ReferenceVariables of identifier
-  | ElimArity of constr * constr list * constr * constr * constr
+  | ElimArity of inductive * constr list * constr * constr * constr
       * (constr * constr * string) option
   | CaseNotInductive of constr * constr
   | NumberBranches of constr * constr * int
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 66242b7cf..7ffbd312e 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -17,7 +17,7 @@ type type_error =
   | NotAType of constr
   | BadAssumption of constr
   | ReferenceVariables of identifier
-  | ElimArity of constr * constr list * constr * constr * constr
+  | ElimArity of inductive * constr list * constr * constr * constr
       * (constr * constr * string) option
   | CaseNotInductive of constr * constr
   | NumberBranches of constr * constr * int
@@ -53,7 +53,7 @@ val error_assumption : path_kind -> env -> constr -> 'b
 val error_reference_variables : path_kind -> env -> identifier -> 'b
 
 val error_elim_arity : 
-  path_kind -> env -> constr -> constr list -> constr 
+  path_kind -> env -> inductive -> constr list -> constr 
     -> constr -> constr -> (constr * constr * string) option -> 'b
 
 val error_case_not_inductive :