diff options
Diffstat (limited to 'pretyping/pretype_errors.ml')
| -rw-r--r-- | pretyping/pretype_errors.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index cc8b0ed8b3..4a60fce3d6 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -24,6 +24,7 @@ type pretype_error = (* Unification *) | OccurCheck of int * constr | NotClean of int * constr + | UnsolvableImplicit of hole_kind (* Pretyping *) | VarNotFound of identifier | UnexpectedType of constr * constr @@ -135,6 +136,9 @@ let error_not_clean env sigma ev c = let c = nf_evar sigma c in raise (PretypeError (env_ise sigma env, NotClean (ev,c))) +let error_unsolvable_implicit loc env sigma e = + raise (PretypeError (env_ise sigma env, UnsolvableImplicit e)) + (*s Ml Case errors *) let error_cant_find_case_type_loc loc env sigma expr = |