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

7 files changed, 21 insertions, 2 deletions

diff --git a/kernel/environ.mli b/kernel/environ.mli
index 3c4dd633ed..cfcdf2d36c 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -48,6 +48,7 @@ val lookup_mind : section_path -> env -> mutual_inductive_body
 val lookup_mind_specif : constr -> env -> mind_specif
 
 val id_of_global : env -> sorts oper -> identifier
+
 val id_of_name_using_hdchar : env -> constr -> name -> identifier
 val named_hd : env -> constr -> name -> name
 val prod_name : env -> name * constr * constr -> constr
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 5ab2886a97..6ae5bb931d 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -157,3 +157,5 @@ let mind_check_lc params mie =
     if not (List.length lna = ntypes) then raise (InductiveError BadEntry)
   in
   List.iter check_lc mie.mind_entry_inds
+
+let inductive_of_constructor (ind_sp,i) = ind_sp
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 1f1d5927fa..63e85a539c 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -106,3 +106,5 @@ val mind_extract_and_check_params :
 val mind_extract_params : int -> constr -> (name * constr) list * constr
 
 val mind_check_lc : (name * constr) list -> mutual_inductive_entry -> unit
+
+val inductive_of_constructor : constructor_path -> inductive_path
diff --git a/kernel/term.ml b/kernel/term.ml
index 38dbc37655..8e9c94c711 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -11,6 +11,8 @@ open Univ
 
 (* Coq abstract syntax with deBruijn variables; 'a is the type of sorts *)
 
+type existential_key = int
+
 type 'a oper = 
   (* DOP0 *)
   | Meta of int
@@ -19,7 +21,7 @@ type 'a oper =
   | Cast | Prod | Lambda
   (* DOPN *)
   | AppL | Const of section_path | Abst of section_path
-  | Evar of int
+  | Evar of existential_key
   | MutInd of inductive_path
   | MutConstruct of constructor_path
   | MutCase of case_info
diff --git a/kernel/term.mli b/kernel/term.mli
index 6e7101ad34..869e65ca40 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -11,12 +11,14 @@ open Generic
   ['a] is the type of sorts. ([XTRA] is an extra slot, for putting in 
   whatever sort of operator we need for whatever sort of application.) *)
 
+type existential_key = int
+
 type 'a oper = 
   | Meta of int
   | Sort of 'a
   | Cast | Prod | Lambda
   | AppL | Const of section_path | Abst of section_path
-  | Evar of int
+  | Evar of existential_key
   | MutInd of inductive_path
   | MutConstruct of constructor_path
   | MutCase of case_info
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index f3cb78205a..89174d1bf6 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -31,6 +31,11 @@ type type_error =
   | CantFindCaseType of constr
   | OccurCheck of int * constr
   | NotClean of int * constr
+  (* Pattern-matching errors *)
+  | BadConstructor of constructor_path * inductive_path
+  | WrongNumargConstructor of constructor_path * int
+  | WrongPredicateArity of constr * int * int
+  | NeedsInversion of constr * constr
 
 exception TypeError of path_kind * context * type_error
 
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 70f444987c..aaf278c271 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -33,6 +33,11 @@ type type_error =
   | CantFindCaseType of constr
   | OccurCheck of int * constr
   | NotClean of int * constr
+  (* Pattern-matching errors *)
+  | BadConstructor of constructor_path * inductive_path
+  | WrongNumargConstructor of constructor_path * int
+  | WrongPredicateArity of constr * int * int
+  | NeedsInversion of constr * constr
 
 exception TypeError of path_kind * context * type_error