diff options
-rw-r--r-- | kernel/type_errors.ml | 1 | ||||
-rw-r--r-- | kernel/type_errors.mli | 1 | ||||
-rw-r--r-- | pretyping/pretype_errors.ml | 3 | ||||
-rw-r--r-- | pretyping/pretype_errors.mli | 3 | ||||
-rw-r--r-- | toplevel/himsg.ml | 7 |
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 |