diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-03 17:14:02 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-03 17:14:02 +0000 |
| commit | 85fb5f33b1cac28e1fe4f00741c66f6f58109f84 (patch) | |
| tree | 4913998a925cb148c74a607bf7523ae1d28853ce /pretyping/pretype_errors.mli | |
| parent | 31ebb89fe48efe92786b1cddc3ba62e7dfc4e739 (diff) | |
premiere reorganisation de l\'unification
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
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 : |