diff options
Diffstat (limited to 'pretyping/pretype_errors.ml')
| -rw-r--r-- | pretyping/pretype_errors.ml | 27 |
1 files changed, 23 insertions, 4 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index fee1522f..48295c92 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pretype_errors.ml,v 1.25.2.2 2004/07/16 19:30:45 herbelin Exp $ *) +(* $Id: pretype_errors.ml 8688 2006-04-07 15:08:12Z msozeau $ *) open Util open Stdpp @@ -24,8 +24,12 @@ type pretype_error = | CantFindCaseType of constr (* Unification *) | OccurCheck of existential_key * constr - | NotClean of existential_key * constr * hole_kind - | UnsolvableImplicit of hole_kind + | NotClean of existential_key * constr * Evd.hole_kind + | UnsolvableImplicit of Evd.hole_kind + | CannotUnify of constr * constr + | CannotUnifyBindingType of constr * constr + | CannotGeneralize of constr + | NoOccurrenceFound of constr (* Pretyping *) | VarNotFound of identifier | UnexpectedType of constr * constr @@ -33,6 +37,12 @@ type pretype_error = exception PretypeError of env * pretype_error +let precatchable_exception = function + | Util.UserError _ | TypeError _ | PretypeError _ + | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | + Nametab.GlobalizationError _ | PretypeError _)) -> true + | _ -> false + let nf_evar = Reductionops.nf_evar let j_nf_evar sigma j = { uj_val = nf_evar sigma j.uj_val; @@ -43,7 +53,7 @@ let tj_nf_evar sigma {utj_val=v;utj_type=t} = {utj_val=type_app (nf_evar sigma) v;utj_type=t} let env_ise sigma env = - let sign = named_context env in + let sign = named_context_val env in let ctxt = rel_context env in let env0 = reset_with_named_context sign env in Sign.fold_rel_context @@ -126,6 +136,9 @@ let error_ill_typed_rec_body_loc loc env sigma i na jl tys = IllTypedRecBody (i,na,jv_nf_evar sigma jl, Array.map (nf_evar sigma) tys)) +let error_not_a_type_loc loc env sigma j = + raise_located_type_error (loc, env, sigma, NotAType (j_nf_evar sigma j)) + (*s Implicit arguments synthesis errors. It is hard to find a precise location. *) @@ -141,6 +154,12 @@ let error_not_clean env sigma ev c (loc,k) = let error_unsolvable_implicit loc env sigma e = raise_with_loc loc (PretypeError (env_ise sigma env, UnsolvableImplicit e)) +let error_cannot_unify env sigma (m,n) = + raise (PretypeError (env_ise sigma env,CannotUnify (m,n))) + +let error_cannot_coerce env sigma (m,n) = + raise (PretypeError (env_ise sigma env,CannotUnify (m,n))) + (*s Ml Case errors *) let error_cant_find_case_type_loc loc env sigma expr = |