Ajout des messages d'erreurs de Cases

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

4 files changed, 42 insertions, 2 deletions

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index c3baf8ea06..083b94df0e 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -18,6 +18,24 @@ let error_ill_formed_branch k env c i actty expty =
 let error_number_branches_loc loc k env c ct expn =
   raise (PretypeError (loc, k, context env, NumberBranches (c,ct,expn)))
 
+let error_case_not_inductive_loc loc k env c ct =
+  raise (PretypeError (loc, k, context env, CaseNotInductive (c,ct)))
+
+(* Pattern-matching errors *)
+
+let error_bad_constructor_loc loc k cstr ind =
+  raise (PretypeError (loc, k, Global.context(), BadConstructor (cstr,ind)))
+
+let error_wrong_numarg_constructor_loc loc k c n =
+  raise (PretypeError (loc, k, Global.context(), WrongNumargConstructor (c,n)))
+
+let error_wrong_predicate_arity_loc loc k env c n1 n2 =
+  raise (PretypeError (loc, k, context env, WrongPredicateArity (c,n1,n2)))
+
+let error_needs_inversion k env x t =
+  raise (TypeError (k, context env, NeedsInversion (x,t)))
+
+
 let error_ill_formed_branch_loc loc k env c i actty expty =
   raise (PretypeError (loc, k, context env, IllFormedBranch (c,i,actty,expty)))
 
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 33238ecd9e..6d39fdd31b 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -24,6 +24,25 @@ val error_ill_formed_branch_loc :
 val error_number_branches_loc : 
   loc -> path_kind -> env -> constr -> constr -> int -> 'b
 
+val error_case_not_inductive_loc :
+  loc -> path_kind -> env -> constr -> constr -> 'b
+
+(* Pattern-matching errors *)
+
+val error_bad_constructor_loc : 
+  loc -> path_kind -> constructor_path -> inductive_path -> 'b
+
+val error_wrong_numarg_constructor_loc : 
+  loc -> path_kind -> constructor_path -> int -> 'b
+
+val error_wrong_predicate_arity_loc :
+  loc -> path_kind -> env -> constr -> int -> int -> 'b
+
+val error_needs_inversion : path_kind -> env -> constr -> constr -> 'a
+
+
+(* Implicit arguments synthesis errors *)
+
 val error_occur_check : path_kind -> env -> int -> constr -> 'a
 
 val error_not_clean : path_kind -> env -> int -> constr -> 'a
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 4978d7b11b..07ea18cdfa 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -18,6 +18,7 @@ type mutind =
     {fullmind : constr;
      mind : mutind_id;
      nparams : int;
+     nrealargs : int;
      nconstr : int;
      params : constr list;
      realargs : constr list;
@@ -28,13 +29,14 @@ let try_mutind_of env sigma ty =
   let (mind,largs) = find_mrectype env sigma ty in
   let mispec = lookup_mind_specif mind env in 
   let nparams = mis_nparams mispec in
-  let (params,proper_args) = list_chop nparams largs in 
+  let (params,realargs) = list_chop nparams largs in 
   {fullmind = ty;
    mind     = (let (sp,i,cv) = destMutInd mind in (sp,i),cv);
    nparams  = nparams;
+   nrealargs = List.length realargs;
    nconstr  = mis_nconstr mispec;
    params   = params;
-   realargs = proper_args;
+   realargs = realargs;
    arity    = Instantiate.mis_arity mispec}
 
 
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index ce9ea73909..354771e6ee 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -33,6 +33,7 @@ type mutind = {
   fullmind : constr;
   mind : mutind_id;
   nparams : int;
+  nrealargs : int;
   nconstr : int;
   params : constr list;
   realargs : constr list;