diff options
Diffstat (limited to 'pretyping/pretype_errors.ml')
| -rw-r--r-- | pretyping/pretype_errors.ml | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 5b829e5bf4..e92ab3206a 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -32,6 +32,8 @@ type pretype_error = | CannotGeneralize of constr | NoOccurrenceFound of constr * identifier option | CannotFindWellTypedAbstraction of constr * constr list + | AbstractionOverMeta of name * name + | NonLinearUnification of name * constr (* Pretyping *) | VarNotFound of identifier | UnexpectedType of constr * constr @@ -174,6 +176,14 @@ let error_cannot_coerce env sigma (m,n) = let error_cannot_find_well_typed_abstraction env sigma p l = raise (PretypeError (env_ise sigma env,CannotFindWellTypedAbstraction (p,l))) +let error_abstraction_over_meta env sigma hdmeta metaarg = + let m = Evd.meta_name sigma hdmeta and n = Evd.meta_name sigma metaarg in + raise (PretypeError (env_ise sigma env,AbstractionOverMeta (m,n))) + +let error_non_linear_unification env sigma hdmeta t = + let m = Evd.meta_name sigma hdmeta in + raise (PretypeError (env_ise sigma env,NonLinearUnification (m,t))) + (*s Ml Case errors *) let error_cant_find_case_type_loc loc env sigma expr = |