diff options
| -rw-r--r-- | kernel/type_errors.ml | 2 | ||||
| -rw-r--r-- | kernel/type_errors.mli | 2 | ||||
| -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, 17 insertions, 0 deletions
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 5806e3364..a79dbcf3c 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -59,6 +59,8 @@ type type_error = | WrongNumargConstructor of constructor_path * int | WrongPredicateArity of constr * int * int | NeedsInversion of constr * constr + (* Relocation error *) + | GlobalNotFound of section_path exception TypeError of path_kind * env * type_error diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 01dbeb535..9a2504ff8 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -63,6 +63,8 @@ type type_error = | WrongNumargConstructor of constructor_path * int | WrongPredicateArity of constr * int * int | NeedsInversion of constr * constr + (* Relocation error *) + | GlobalNotFound of section_path exception TypeError of path_kind * env * type_error diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 04a5bd0ff..594f3fc9e 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -13,6 +13,9 @@ let raise_pretype_error (loc,k,ctx,te) = let error_var_not_found_loc loc k s = raise_pretype_error (loc,k, Global.env() (*bidon*), VarNotFound s) +let error_global_not_found_loc loc sp = + raise_pretype_error (loc,CCI, Global.env() (*bidon*), GlobalNotFound sp) + let error_cant_find_case_type_loc loc env expr = raise_pretype_error (loc, CCI, env, CantFindCaseType expr) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index a061cd57e..c670e1f97 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -16,6 +16,9 @@ open Rawterm val error_var_not_found_loc : loc -> path_kind -> identifier -> 'a +val error_global_not_found_loc : + loc -> section_path -> 'a + val error_cant_find_case_type_loc : loc -> env -> constr -> 'a diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index a4a089bd5..449b7bc1e 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -279,6 +279,11 @@ let explain_var_not_found k ctx id = 'sPC ; 'sTR "was not found"; 'sPC ; 'sTR "in the current"; 'sPC ; 'sTR "environment" >] +let explain_global_not_found k ctx sp = + [< 'sTR "The reference"; 'sPC; 'sTR (string_of_path sp); + 'sPC ; 'sTR "was not found"; + '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 @@ -355,6 +360,8 @@ let explain_type_error k ctx = function explain_not_clean k ctx n c | VarNotFound id -> explain_var_not_found k ctx id + | GlobalNotFound sp -> + explain_global_not_found k ctx sp | UnexpectedType (actual,expected) -> explain_unexpected_type k ctx actual expected | NotProduct c -> |