diff options
Diffstat (limited to 'kernel/type_errors.ml')
| -rw-r--r-- | kernel/type_errors.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 481ffc290c..814ef8bdfc 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -64,6 +64,7 @@ type ('constr, 'types) ptype_error = int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array | UnsatisfiedConstraints of Univ.Constraint.t | UndeclaredUniverse of Univ.Level.t + | DisallowedSProp type type_error = (constr, types) ptype_error @@ -149,6 +150,9 @@ let error_unsatisfied_constraints env c = let error_undeclared_universe env l = raise (TypeError (env, UndeclaredUniverse l)) +let error_disallowed_sprop env = + raise (TypeError (env, DisallowedSProp)) + let map_pguard_error f = function | NotEnoughAbstractionInFixBody -> NotEnoughAbstractionInFixBody | RecursionNotOnInductiveType c -> RecursionNotOnInductiveType (f c) @@ -189,3 +193,4 @@ let map_ptype_error f = function IllTypedRecBody (n, na, Array.map (on_judgment f) jv, Array.map f t) | UnsatisfiedConstraints g -> UnsatisfiedConstraints g | UndeclaredUniverse l -> UndeclaredUniverse l +| DisallowedSProp -> DisallowedSProp |