diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-12 17:53:35 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-12 17:53:35 +0000 |
commit | a97decb77b2084a3b84c5135f5bae2dbbb5ace26 (patch) | |
tree | cdaf12b9b4b4470ed561871f238a6fd8d4526907 /pretyping/pretype_errors.ml | |
parent | deec843772d392f71806c011351fa6d4f551115d (diff) |
Fixed bug #2135 (second-order unification was raising cryptic message)
- made the example work (a call to whd_meta was missing)
- replaced the internal error messages of w_unify_to_subterm_list into
user-understandable messages
- incidentally fixed the meaning of whd_meta (which now takes an evd)
and meta_name (which now does what it means and do not treat differently
the instantiated metas)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13122 85f007b7-540e-0410-9357-904b9bb8a0f7
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 5b829e5bf..e92ab3206 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 = |