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 dc6607557d..1a51ea4db7 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -60,6 +60,7 @@ type pretype_error = | CannotUnifyOccurrences of subterm_unification_error | UnsatisfiableConstraints of (Evar.t * Evar_kinds.t) option * Evar.Set.t option + | DisallowedSProp exception PretypeError of env * Evd.evar_map * pretype_error @@ -171,6 +172,9 @@ let error_var_not_found ?loc env sigma s = let error_evar_not_found ?loc env sigma id = raise_pretype_error ?loc (env, sigma, EvarNotFound id) +let error_disallowed_sprop env sigma = + raise (PretypeError (env, sigma, DisallowedSProp)) + (*s Typeclass errors *) let unsatisfiable_constraints env evd ev comp = |