Add a non-cumulative impredicative universe SProp.

Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.

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