diff options
Diffstat (limited to 'pretyping/pretype_errors.mli')
-rw-r--r-- | pretyping/pretype_errors.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index e09a6d1d1..2f9b1dc46 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -28,6 +28,9 @@ type pretype_error = | OccurCheck of existential_key * constr | NotClean of existential_key * constr * hole_kind | UnsolvableImplicit of hole_kind + | CannotUnify of constr * constr + | CannotGeneralize of constr + | NoOccurrenceFound of constr (* Pretyping *) | VarNotFound of identifier | UnexpectedType of constr * constr @@ -35,6 +38,8 @@ type pretype_error = exception PretypeError of env * pretype_error +val precatchable_exception : exn -> bool + (* Presenting terms without solved evars *) val nf_evar : Evd.evar_map -> constr -> constr val j_nf_evar : Evd.evar_map -> unsafe_judgment -> unsafe_judgment @@ -82,6 +87,8 @@ val error_not_clean : val error_unsolvable_implicit : loc -> env -> Evd.evar_map -> hole_kind -> 'b +val error_cannot_unify : env -> Evd.evar_map -> constr * constr -> 'b + (*s Ml Case errors *) val error_cant_find_case_type_loc : |