Messages d'erreurs Cases

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

5 files changed, 15 insertions, 0 deletions

diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 34dee81c8..f96b0b9a1 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -54,6 +54,7 @@ type type_error =
   | UnexpectedType of constr * constr
   | NotProduct of constr
   (* Pattern-matching errors *)
+  | BadPattern of constructor * constr
   | BadConstructor of constructor * inductive
   | WrongNumargConstructor of constructor_path * int
   | WrongPredicateArity of constr * int * int
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index f5e16f3c4..d8031350c 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -58,6 +58,7 @@ type type_error =
   | UnexpectedType of constr * constr
   | NotProduct of constr
   (* Pattern-matching errors *)
+  | BadPattern of constructor * constr
   | BadConstructor of constructor * inductive
   | WrongNumargConstructor of constructor_path * int
   | WrongPredicateArity of constr * int * int
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index b8a080366..04a5bd0ff 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -37,6 +37,9 @@ let error_case_not_inductive_loc loc k env c ct =
 
 (* Pattern-matching errors *)
 
+let error_bad_pattern_loc loc k cstr ind =
+  raise_pretype_error (loc, k, Global.env(), BadPattern (cstr,ind))
+
 let error_bad_constructor_loc loc k cstr ind =
   raise_pretype_error (loc, k, Global.env(), BadConstructor (cstr,ind))
 
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index aab6abc08..a061cd57e 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -40,6 +40,9 @@ val error_case_not_inductive_loc :
 
 (*s Pattern-matching errors *)
 
+val error_bad_pattern_loc : 
+  loc -> path_kind -> constructor -> constr -> 'b
+
 val error_bad_constructor_loc : 
   loc -> path_kind -> constructor -> inductive -> 'b
 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index f40cc5eee..7b1f3cf8c 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -281,6 +281,13 @@ let explain_var_not_found k ctx id =
      'sPC ; 'sTR "in the current"; 'sPC ; 'sTR "environment" >]
 
 (* Pattern-matching errors *)
+let explain_bad_pattern k ctx cstr ty = 
+  let pt = prterm_env ctx ty in
+  let pc = pr_constructor ctx cstr in
+  [< 'sTR "Found the constructor "; pc; 'bRK(1,1); 
+     'sTR "while matching a term of type "; pt; 'bRK(1,1); 
+     'sTR "which is not an inductive type" >]
+
 let explain_bad_constructor k ctx cstr ind =
   let pi = pr_inductive ctx ind in
   let pc = pr_constructor ctx cstr in