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.

22 files changed, 209 insertions, 71 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index af14baaca6..69f004307d 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -550,7 +550,7 @@ let rec compile_lam env cenv lam sz cont =
     else comp_app compile_structured_constant compile_universe cenv
         (Const_ind ind) (Univ.Instance.to_array u) sz cont
 
-  | Lsort (Sorts.Prop | Sorts.Set as s) ->
+  | Lsort (Sorts.SProp | Sorts.Prop | Sorts.Set as s) ->
     compile_structured_constant cenv (Const_sort s) sz cont
   | Lsort (Sorts.Type u) ->
     (* We represent universes as a global constant with local universes
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index 5c21a5ec25..d2147884ba 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -55,6 +55,7 @@ let pp_sort s =
   match Sorts.family s with
   | InSet -> str "Set"
   | InProp -> str "Prop"
+  | InSProp -> str "SProp"
   | InType -> str "Type"
 
 let rec pp_lam lam =
diff --git a/kernel/environ.ml b/kernel/environ.ml
index ab046f02f7..5f6d5f3d0e 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -59,7 +59,8 @@ type globals = {
 
 type stratification = {
   env_universes : UGraph.t;
-  env_engagement : engagement
+  env_engagement : engagement;
+  env_sprop_allowed : bool;
 }
 
 type val_kind =
@@ -117,7 +118,9 @@ let empty_env = {
   env_nb_rel = 0;
   env_stratification = {
     env_universes = UGraph.initial_universes;
-    env_engagement = PredicativeSet };
+    env_engagement = PredicativeSet;
+    env_sprop_allowed = false;
+  };
   env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
   retroknowledge = Retroknowledge.empty;
   indirect_pterms = Opaqueproof.empty_opaquetab }
@@ -243,7 +246,7 @@ let is_impredicative_set env =
   | _ -> false
 
 let is_impredicative_sort env = function
-  | Sorts.Prop -> true
+  | Sorts.SProp | Sorts.Prop -> true
   | Sorts.Set -> is_impredicative_set env
   | Sorts.Type _ -> false
 
@@ -432,6 +435,14 @@ let set_typing_flags c env = (* Unsafe *)
   if same_flags env.env_typing_flags c then env
   else { env with env_typing_flags = c }
 
+let make_sprop_cumulative = map_universes UGraph.make_sprop_cumulative
+
+let set_allow_sprop b env =
+  { env with env_stratification =
+    { env.env_stratification with env_sprop_allowed = b } }
+
+let sprop_allowed env = env.env_stratification.env_sprop_allowed
+
 (* Global constants *)
 
 let no_link_info = NotLinked
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 0df9b91c4a..8c6bc105c7 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -51,7 +51,8 @@ type globals
 
 type stratification = {
   env_universes : UGraph.t;
-  env_engagement : engagement
+  env_engagement : engagement;
+  env_sprop_allowed : bool;
 }
 
 type named_context_val = private {
@@ -290,6 +291,9 @@ val push_subgraph : Univ.ContextSet.t -> env -> env
 
 val set_engagement : engagement -> env -> env
 val set_typing_flags : typing_flags -> env -> env
+val make_sprop_cumulative : env -> env
+val set_allow_sprop : bool -> env -> env
+val sprop_allowed : env -> bool
 
 val universes_of_global : env -> GlobRef.t -> AUContext.t
 
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index a5dafc5ab5..0d63c8feba 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -199,9 +199,10 @@ let check_constructors env_ar_par params lc (arity,indices,univ_info) =
 (* - all_sorts in case of small, unitary Prop (not smashed) *)
 (* - logical_sorts in case of large, unitary Prop (smashed) *)
 
-let all_sorts = [InProp;InSet;InType]
-let small_sorts = [InProp;InSet]
-let logical_sorts = [InProp]
+let all_sorts = [InSProp;InProp;InSet;InType]
+let small_sorts = [InSProp;InProp;InSet]
+let logical_sorts = [InSProp;InProp]
+let sprop_sorts = [InSProp]
 
 let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_} =
   if not ind_squashed then all_sorts
@@ -209,6 +210,7 @@ let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_} =
     | InType -> assert false
     | InSet -> small_sorts
     | InProp -> logical_sorts
+    | InSProp -> sprop_sorts
 
 (* Returns the list [x_1, ..., x_n] of levels contributing to template
    polymorphism. The elements x_k is None if the k-th parameter (starting
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index d14a212de0..66cd4cba9e 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -226,7 +226,10 @@ let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args =
 (* The max of an array of universes *)
 
 let cumulate_constructor_univ u = let open Sorts in function
-  | Prop -> u
+  | SProp | Prop ->
+    (* SProp is non cumulative but allowed in constructors of any
+       inductive (except non-sprop primitive records) *)
+    u
   | Set -> Universe.sup Universe.type0 u
   | Type u' -> Universe.sup u u'
 
@@ -301,11 +304,7 @@ let build_dependent_inductive ind (_,mip) params =
 exception LocalArity of (Sorts.family * Sorts.family * arity_error) option
 
 let check_allowed_sort ksort specif =
-  let open Sorts in
-  let eq_ksort s = match ksort, s with
-  | InProp, InProp | InSet, InSet | InType, InType -> true
-  | _ -> false in
-  if not (CList.exists eq_ksort (elim_sorts specif)) then
+  if not (CList.exists (Sorts.family_equal ksort) (elim_sorts specif)) then
     let s = inductive_sort_family (snd specif) in
     raise (LocalArity (Some(ksort,s,error_elim_explain ksort s)))
 
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 414fc0dc28..3eb51ffc59 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -117,7 +117,7 @@ let mk_ind_accu ind u =
 let mk_sort_accu s u =
   let open Sorts in
   match s with
-  | Prop | Set -> mk_accu (Asort s)
+  | SProp | Prop | Set -> mk_accu (Asort s)
   | Type s ->
      let u = Univ.Instance.of_array u in
      let s = Sorts.sort_of_univ (Univ.subst_instance_universe u s) in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index b583d33e29..d526b25e5b 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -701,7 +701,8 @@ let check_sort_cmp_universes env pb s0 s1 univs =
       | CONV -> check_eq univs u0 u1
     in
     match (s0,s1) with
-    | Prop, Prop | Set, Set -> ()
+    | SProp, SProp | Prop, Prop | Set, Set -> ()
+    | SProp, _ | _, SProp -> raise NotConvertible
     | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible
     | Set, Prop -> raise NotConvertible
     | Set, Type u -> check_pb Univ.type0_univ u
@@ -749,7 +750,8 @@ let infer_cmp_universes env pb s0 s1 univs =
       | CONV -> infer_eq univs u0 u1
     in
     match (s0,s1) with
-    | Prop, Prop | Set, Set -> univs
+    | SProp, SProp | Prop, Prop | Set, Set -> univs
+    | SProp, _ | _, SProp -> raise NotConvertible
     | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible else univs
     | Set, Prop -> raise NotConvertible
     | Set, Type u -> infer_pb Univ.type0_univ u
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a05f7b9b04..badd8d320f 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -211,6 +211,10 @@ let set_native_compiler b senv =
   let flags = Environ.typing_flags senv.env in
   set_typing_flags { flags with enable_native_compiler = b } senv
 
+let make_sprop_cumulative senv = { senv with env = Environ.make_sprop_cumulative senv.env }
+
+let set_allow_sprop b senv = { senv with env = Environ.set_allow_sprop b senv.env }
+
 (** Check that the engagement [c] expected by a library matches
     the current (initial) one *)
 let check_engagement env expected_impredicative_set =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 8539fdd504..46c97c1fb8 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -141,6 +141,8 @@ val set_typing_flags : Declarations.typing_flags -> safe_transformer0
 val set_share_reduction : bool -> safe_transformer0
 val set_VM : bool -> safe_transformer0
 val set_native_compiler : bool -> safe_transformer0
+val make_sprop_cumulative : safe_transformer0
+val set_allow_sprop : bool -> safe_transformer0
 
 val check_engagement : Environ.env -> Declarations.set_predicativity -> unit
 
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index e281751be1..1e4e4e00b4 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -10,13 +10,15 @@
 
 open Univ
 
-type family = InProp | InSet | InType
+type family = InSProp | InProp | InSet | InType
 
 type t =
+  | SProp
   | Prop
   | Set
   | Type of Universe.t
 
+let sprop = SProp
 let prop = Prop
 let set = Set
 let type1 = Type type1_univ
@@ -25,15 +27,20 @@ let univ_of_sort = function
   | Type u -> u
   | Set -> Universe.type0
   | Prop -> Universe.type0m
+  | SProp -> Universe.sprop
 
 let sort_of_univ u =
-  if is_type0m_univ u then prop
+  if Universe.is_sprop u then sprop
+  else if is_type0m_univ u then prop
   else if is_type0_univ u then set
   else Type u
 
 let compare s1 s2 =
   if s1 == s2 then 0 else
     match s1, s2 with
+    | SProp, SProp -> 0
+    | SProp, _ -> -1
+    | _, SProp -> 1
     | Prop, Prop -> 0
     | Prop, _ -> -1
     | Set, Prop -> 1
@@ -45,33 +52,51 @@ let compare s1 s2 =
 let equal s1 s2 = Int.equal (compare s1 s2) 0
 
 let super = function
-  | Prop | Set -> Type (Universe.type1)
+  | SProp | Prop | Set -> Type (Universe.type1)
   | Type u -> Type (Universe.super u)
 
+let is_sprop = function
+  | SProp -> true
+  | Prop | Set | Type _ -> false
+
 let is_prop = function
   | Prop -> true
-  | Set | Type _ -> false
+  | SProp | Set | Type _ -> false
 
 let is_set = function
   | Set -> true
-  | Prop | Type _ -> false
+  | SProp | Prop | Type _ -> false
 
 let is_small = function
-  | Prop | Set -> true
+  | SProp | Prop | Set -> true
   | Type _ -> false
 
 let family = function
+  | SProp -> InSProp
   | Prop -> InProp
   | Set -> InSet
   | Type _ -> InType
 
+let family_compare a b = match a,b with
+  | InSProp, InSProp -> 0
+  | InSProp, _ -> -1
+  | _, InSProp -> 1
+  | InProp, InProp -> 0
+  | InProp, _ -> -1
+  | _, InProp -> 1
+  | InSet, InSet -> 0
+  | InSet, _ -> -1
+  | _, InSet -> 1
+  | InType, InType -> 0
+
 let family_equal = (==)
 
 open Hashset.Combine
 
 let hash = function
-  | Prop -> combinesmall 1 0
-  | Set -> combinesmall 1 1
+  | SProp -> combinesmall 1 0
+  | Prop -> combinesmall 1 1
+  | Set -> combinesmall 1 2
   | Type u ->
     let h = Univ.Universe.hash u in
     combinesmall 2 h
@@ -104,11 +129,13 @@ module Hsorts =
 let hcons = Hashcons.simple_hcons Hsorts.generate Hsorts.hcons hcons_univ
 
 let debug_print = function
-  | Set -> Pp.(str "Set")
+  | SProp -> Pp.(str "SProp")
   | Prop -> Pp.(str "Prop")
+  | Set -> Pp.(str "Set")
   | Type u -> Pp.(str "Type(" ++ Univ.Universe.pr u ++ str ")")
 
 let pr_sort_family = function
-  | InSet -> Pp.(str "Set")
+  | InSProp -> Pp.(str "SProp")
   | InProp -> Pp.(str "Prop")
+  | InSet -> Pp.(str "Set")
   | InType -> Pp.(str "Type")
diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index 3ca76645db..65078c2a62 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -10,13 +10,15 @@
 
 (** {6 The sorts of CCI. } *)
 
-type family = InProp | InSet | InType
+type family = InSProp | InProp | InSet | InType
 
 type t = private
+  | SProp
   | Prop
   | Set
   | Type of Univ.Universe.t
 
+val sprop : t
 val set  : t
 val prop : t
 val type1  : t
@@ -25,6 +27,7 @@ val equal : t -> t -> bool
 val compare : t -> t -> int
 val hash : t -> int
 
+val is_sprop : t -> bool
 val is_set : t -> bool
 val is_prop : t -> bool
 val is_small : t -> bool
@@ -32,6 +35,7 @@ val family : t -> family
 
 val hcons : t -> t
 
+val family_compare : family -> family -> int
 val family_equal : family -> family -> bool
 
 module List : sig
diff --git a/kernel/term.ml b/kernel/term.ml
index d791fe67e5..e67c2130d5 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -16,11 +16,11 @@ open Vars
 open Constr
 
 (* Deprecated *)
-type sorts_family = Sorts.family = InProp | InSet | InType
+type sorts_family = Sorts.family = InSProp | InProp | InSet | InType
 [@@ocaml.deprecated "Alias for Sorts.family"]
 
 type sorts = Sorts.t = private
-  | Prop | Set
+  | SProp | Prop | Set
   | Type of Univ.Universe.t  (** Type *)
 [@@ocaml.deprecated "Alias for Sorts.t"]
 
diff --git a/kernel/term.mli b/kernel/term.mli
index 2150f21ed1..7fa817bada 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -190,10 +190,10 @@ type ('constr, 'types) kind_of_type =
 val kind_of_type : types -> (constr, types) kind_of_type
 
 (* Deprecated *)
-type sorts_family = Sorts.family = InProp | InSet | InType
+type sorts_family = Sorts.family = InSProp | InProp | InSet | InType
 [@@ocaml.deprecated "Alias for Sorts.family"]
 
 type sorts = Sorts.t = private
-  | Prop | Set
+  | SProp | Prop | Set
   | Type of Univ.Universe.t  (** Type *)
 [@@ocaml.deprecated "Alias for Sorts.t"]
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
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index c5ab9a4e73..e208c57e0a 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -65,6 +65,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
 
@@ -134,5 +135,7 @@ val error_unsatisfied_constraints : env -> Univ.Constraint.t -> 'a
 
 val error_undeclared_universe : env -> Univ.Level.t -> 'a
 
+val error_disallowed_sprop : env -> 'a
+
 val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
 val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 6d12ce3020..1232ab654e 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -69,7 +69,7 @@ let type_of_type u =
     mkType uu
 
 let type_of_sort = function
-  | Prop | Set -> type1
+  | SProp | Prop | Set -> type1
   | Type u -> type_of_type u
 
 (*s Type of a de Bruijn index. *)
@@ -264,6 +264,7 @@ let judge_of_int env i =
 
 let sort_of_product env domsort rangsort =
   match (domsort, rangsort) with
+    | (_, SProp) | (SProp, _) -> rangsort
     (* Product rule (s,Prop,Prop) *)
     | (_,       Prop)  -> rangsort
     (* Product rule (Prop/Set,Set,Set) *)
@@ -463,7 +464,11 @@ let rec execute env cstr =
   let open Context.Rel.Declaration in
   match kind cstr with
     (* Atomic terms *)
-    | Sort s -> type_of_sort s
+    | Sort s ->
+      (match s with
+       | SProp -> if not (Environ.sprop_allowed env) then error_disallowed_sprop env
+       | _ -> ());
+      type_of_sort s
 
     | Rel n ->
       type_of_relative env n
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 8187dea41b..0d5b55ca1b 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -29,15 +29,22 @@ module G = AcyclicGraph.Make(struct
    code (eg add_universe with a constraint vs G.add with no
    constraint) *)
 
-type t = G.t
-type 'a check_function = 'a G.check_function
+type t = { graph: G.t; sprop_cumulative : bool }
+type 'a check_function = t -> 'a -> 'a -> bool
+
+let g_map f g =
+  let g' = f g.graph in
+  if g.graph == g' then g
+  else {g with graph=g'}
+
+let make_sprop_cumulative g = {g with sprop_cumulative=true}
 
 let check_smaller_expr g (u,n) (v,m) =
   let diff = n - m in
     match diff with
-    | 0 -> G.check_leq g u v
-    | 1 -> G.check_lt g u v
-    | x when x < 0 -> G.check_leq g u v
+    | 0 -> G.check_leq g.graph u v
+    | 1 -> G.check_lt g.graph u v
+    | x when x < 0 -> G.check_leq g.graph u v
     | _ -> false
 
 let exists_bigger g ul l =
@@ -48,24 +55,28 @@ let real_check_leq g u v =
   Universe.for_all (fun ul -> exists_bigger g ul v) u
 
 let check_leq g u v =
-  Universe.equal u v ||
-    is_type0m_univ u ||
-    real_check_leq g u v
+  Universe.equal u v || (g.sprop_cumulative && Universe.is_sprop u) ||
+  (not (Universe.is_sprop u) && not (Universe.is_sprop v) &&
+    (is_type0m_univ u ||
+     real_check_leq g u v))
 
 let check_eq g u v =
   Universe.equal u v ||
-  (real_check_leq g u v && real_check_leq g v u)
+  (not (Universe.is_sprop u || Universe.is_sprop v) &&
+   (real_check_leq g u v && real_check_leq g v u))
 
-let check_eq_level = G.check_eq
+let check_eq_level g u v =
+  u == v ||
+  (not (Level.is_sprop u || Level.is_sprop v) && G.check_eq g.graph u v)
 
-let empty_universes = G.empty
+let empty_universes = {graph=G.empty; sprop_cumulative=false}
 
 let initial_universes =
   let big_rank = 1000000 in
   let g = G.empty in
   let g = G.add ~rank:big_rank Level.prop g in
   let g = G.add ~rank:big_rank Level.set g in
-  G.enforce_lt Level.prop Level.set g
+  {graph=G.enforce_lt Level.prop Level.set g; sprop_cumulative=false}
 
 let enforce_constraint (u,d,v) g =
   match d with
@@ -73,6 +84,13 @@ let enforce_constraint (u,d,v) g =
   | Lt -> G.enforce_lt u v g
   | Eq -> G.enforce_eq u v g
 
+let enforce_constraint (u,d,v as cst) g =
+  match Level.is_sprop u, d, Level.is_sprop v with
+  | false, _, false -> g_map (enforce_constraint cst) g
+  | true, (Eq|Le), true -> g
+  | true, Le, false when g.sprop_cumulative -> g
+  | _ ->  raise (UniverseInconsistency (d,Universe.make u, Universe.make v, None))
+
 let merge_constraints csts g = Constraint.fold enforce_constraint csts g
 
 let check_constraint g (u,d,v) =
@@ -81,6 +99,13 @@ let check_constraint g (u,d,v) =
   | Lt -> G.check_lt g u v
   | Eq -> G.check_eq g u v
 
+let check_constraint g (u,d,v as cst) =
+  match Level.is_sprop u, d, Level.is_sprop v with
+  | false, _, false -> check_constraint g.graph cst
+  | true, (Eq|Le), true -> true
+  | true, Le, false -> g.sprop_cumulative
+  | _ -> false
+
 let check_constraints csts g = Constraint.for_all (check_constraint g) csts
 
 let leq_expr (u,m) (v,n) =
@@ -125,17 +150,17 @@ let enforce_leq_alg u v g =
 
 exception AlreadyDeclared = G.AlreadyDeclared
 let add_universe u strict g =
-  let g = G.add u g in
+  let graph = G.add u g.graph in
   let d = if strict then Lt else Le in
-  enforce_constraint (Level.set,d,u) g
+  enforce_constraint (Level.set,d,u) {g with graph}
 
-let add_universe_unconstrained u g = G.add u g
+let add_universe_unconstrained u g = {g with graph=G.add u g.graph}
 
 exception UndeclaredLevel = G.Undeclared
-let check_declared_universes = G.check_declared
+let check_declared_universes g l = G.check_declared g.graph (LSet.remove Level.sprop l)
 
-let constraints_of_universes = G.constraints_of
-let constraints_for = G.constraints_for
+let constraints_of_universes g = G.constraints_of g.graph
+let constraints_for ~kept g = G.constraints_for ~kept:(LSet.remove Level.sprop kept) g.graph
 
 (** Subtyping of polymorphic contexts *)
 
@@ -160,18 +185,20 @@ let check_eq_instances g t1 t2 =
           (Int.equal i (Array.length t1)) || (check_eq_level g t1.(i) t2.(i) && aux (i + 1))
         in aux 0)
 
-let domain = G.domain
-let choose = G.choose
+let domain g = LSet.add Level.sprop (G.domain g.graph)
+let choose p g u = if Level.is_sprop u
+  then if p u then Some u else None
+  else G.choose p g.graph u
 
-let dump_universes = G.dump
+let dump_universes f g = G.dump f g.graph
 
-let check_universes_invariants g = G.check_invariants ~required_canonical:Level.is_small g
+let check_universes_invariants g = G.check_invariants ~required_canonical:Level.is_small g.graph
 
-let pr_universes = G.pr
+let pr_universes prl g = G.pr prl g.graph
 
 let dummy_mp = Names.DirPath.make [Names.Id.of_string "Type"]
 let make_dummy i = Level.(make (UGlobal.make dummy_mp i))
-let sort_universes g = G.sort make_dummy [Level.prop;Level.set] g
+let sort_universes g = g_map (G.sort make_dummy [Level.prop;Level.set]) g
 
 (** Profiling *)
 
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index e1a5d50425..17d6c6e6d3 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -13,6 +13,9 @@ open Univ
 (** {6 Graphs of universes. } *)
 type t
 
+val make_sprop_cumulative : t -> t
+(** Don't use this in the kernel, it makes the system incomplete. *)
+
 type 'a check_function = t -> 'a -> 'a -> bool
 
 val check_leq : Universe.t check_function
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 09bf695915..8263c68bf5 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -53,6 +53,7 @@ struct
   end
 
   type t =
+    | SProp
     | Prop
     | Set
     | Level of UGlobal.t
@@ -63,6 +64,7 @@ struct
   let equal x y =
     x == y ||
       match x, y with
+      | SProp, SProp -> true
       | Prop, Prop -> true
       | Set, Set -> true
       | Level l, Level l' -> UGlobal.equal l l'
@@ -71,6 +73,9 @@ struct
 
   let compare u v =
     match u, v with
+    | SProp, SProp -> 0
+    | SProp, _ -> -1
+    | _, SProp -> 1
     | Prop,Prop -> 0
     | Prop, _ -> -1
     | _, Prop -> 1
@@ -88,6 +93,7 @@ struct
   let hequal x y =
     x == y ||
       match x, y with
+      | SProp, SProp -> true
       | Prop, Prop -> true
       | Set, Set -> true
       | Level (n,d), Level (n',d') ->
@@ -96,6 +102,7 @@ struct
       | _ -> false
 
   let hcons = function
+    | SProp as x -> x
     | Prop as x -> x
     | Set as x -> x
     | Level (d,n) as x ->
@@ -106,8 +113,9 @@ struct
   open Hashset.Combine
 
   let hash = function
-    | Prop -> combinesmall 1 0
-    | Set -> combinesmall 1 1
+    | SProp -> combinesmall 1 0
+    | Prop -> combinesmall 1 1
+    | Set -> combinesmall 1 2
     | Var n -> combinesmall 2 n
     | Level (d, n) -> combinesmall 3 (combine n (Names.DirPath.hash d))
 
@@ -118,6 +126,7 @@ module Level = struct
   module UGlobal = RawLevel.UGlobal
 
   type raw_level = RawLevel.t =
+  | SProp
   | Prop
   | Set
   | Level of UGlobal.t
@@ -155,11 +164,13 @@ module Level = struct
 
   let set = make Set
   let prop = make Prop
+  let sprop = make SProp
 
   let is_small x = 
     match data x with
     | Level _ -> false
     | Var _ -> false
+    | SProp -> true
     | Prop -> true
     | Set -> true
  
@@ -173,12 +184,18 @@ module Level = struct
     | Set -> true
     | _ -> false
 
+  let is_sprop x =
+    match data x with
+    | SProp -> true
+    | _ -> false
+
   let compare u v =
     if u == v then 0
     else RawLevel.compare (data u) (data v)
 	    
   let to_string x = 
     match data x with
+    | SProp -> "SProp"
     | Prop -> "Prop"
     | Set -> "Set"
     | Level (d,n) -> Names.DirPath.to_string d^"."^string_of_int n
@@ -188,6 +205,7 @@ module Level = struct
 
   let apart u v =
     match data u, data v with
+    | SProp, _ | _, SProp
     | Prop, Set | Set, Prop -> true
     | _ -> false
 
@@ -308,6 +326,7 @@ struct
 	  if Int.equal n n' then Level.compare x x'
 	  else n - n'
 
+    let sprop = hcons (Level.sprop, 0)
     let prop = hcons (Level.prop, 0)
     let set = hcons (Level.set, 0)
     let type1 = hcons (Level.set, 1)
@@ -326,16 +345,16 @@ struct
       let cmp = Level.compare u v in
 	if Int.equal cmp 0 then n <= n'
 	else if n <= n' then 
-	  (Level.is_prop u && Level.is_small v)
+          (Level.is_prop u && not (Level.is_sprop v))
 	else false
 
     let successor (u,n) =
-      if Level.is_prop u then type1
+      if Level.is_small u then type1
       else (u, n + 1)
 
     let addn k (u,n as x) = 
       if k = 0 then x 
-      else if Level.is_prop u then
+      else if Level.is_small u then
 	(Level.set,n+k)
       else (u,n+k)
 
@@ -353,13 +372,16 @@ struct
        left expression is "smaller" than the right one in both cases. *)
     let super (u,n) (v,n') =
       let cmp = Level.compare u v in
-	if Int.equal cmp 0 then SuperSame (n < n')
+        if Int.equal cmp 0 then SuperSame (n < n')
 	else
           let open RawLevel in
           match Level.data u, n, Level.data v, n' with
-          | Prop, _, Prop, _ -> SuperSame (n < n')
-          | Prop, 0, _, _ -> SuperSame true
-          | _, _, Prop, 0 -> SuperSame false
+          | SProp, _, SProp, _ | Prop, _, Prop, _ -> SuperSame (n < n')
+          | SProp, 0, Prop, 0 -> SuperSame true
+          | Prop, 0, SProp, 0 -> SuperSame false
+          | (SProp | Prop), 0, _, _ -> SuperSame true
+          | _, _, (SProp | Prop), 0 -> SuperSame false
+
           | _, _, _, _ -> SuperDiff cmp
 
     let to_string (v, n) =
@@ -445,6 +467,8 @@ struct
     | [l] -> Expr.is_small l
     | _ -> false
 
+  let sprop = tip Expr.sprop
+
   (* The lower predicative level of the hierarchy that contains (impredicative)
      Prop and singleton inductive types *)
   let type0m = tip Expr.prop
@@ -454,8 +478,9 @@ struct
 
   (* When typing [Prop] and [Set], there is no constraint on the level,
      hence the definition of [type1_univ], the type of [Prop] *)    
-  let type1 = tip (Expr.successor Expr.set)
+  let type1 = tip Expr.type1
 
+  let is_sprop x = equal sprop x
   let is_type0m x = equal type0m x
   let is_type0 x = equal type0 x
 
@@ -656,7 +681,7 @@ let enforce_eq u v c =
 let constraint_add_leq v u c =
   (* We just discard trivial constraints like u<=u *)
   if Expr.equal v u then c
-  else 
+  else
     match v, u with
     | (x,n), (y,m) -> 
     let j = m - n in
@@ -679,7 +704,12 @@ let check_univ_leq u v =
   Universe.for_all (fun u -> check_univ_leq_one u v) u
 
 let enforce_leq u v c =
-  List.fold_left (fun c v -> (List.fold_left (fun c u -> constraint_add_leq u v c) c u)) c v
+  match is_sprop u, is_sprop v with
+  | true, true -> c
+  | true, false | false, true ->
+    raise (UniverseInconsistency (Le, u, v, None))
+  | false, false ->
+    List.fold_left (fun c v -> (List.fold_left (fun c u -> constraint_add_leq u v c) c u)) c v
 
 let enforce_leq u v c =
   if check_univ_leq u v then c
@@ -845,7 +875,7 @@ struct
     else Array.append x y
 
   let of_array a =
-    assert(Array.for_all (fun x -> not (Level.is_prop x)) a);
+    assert(Array.for_all (fun x -> not (Level.is_prop x || Level.is_sprop x)) a);
     a
 
   let to_array a = a
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 1fbebee350..5543c35741 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -30,11 +30,13 @@ sig
 
   val set : t
   val prop : t
+  val sprop : t
   (** The set and prop universe levels. *)
 
   val is_small : t -> bool
   (** Is the universe set or prop? *)
 
+  val is_sprop : t -> bool
   val is_prop : t -> bool
   val is_set : t -> bool
   (** Is it specifically Prop or Set *)
@@ -119,6 +121,8 @@ sig
   val sup   : t -> t -> t
   (** The l.u.b. of 2 universes *)
 
+  val sprop : t
+
   val type0m : t
   (** image of Prop in the universes hierarchy *)
 
@@ -128,6 +132,10 @@ sig
   val type1 : t
   (** the universe of the type of Prop/Set *)
 
+  val is_sprop : t -> bool
+  val is_type0m : t -> bool
+  val is_type0 : t -> bool
+
   val exists : (Level.t * int -> bool) -> t -> bool
   val for_all : (Level.t * int -> bool) -> t -> bool
 
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index ac5350e9fa..777a207013 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -137,6 +137,7 @@ let hash_annot_switch asw =
 let pp_sort s =
   let open Sorts in
   match s with
+  | SProp -> Pp.str "SProp"
   | Prop -> Pp.str "Prop"
   | Set -> Pp.str "Set"
   | Type u -> Pp.(str "Type@{" ++ Univ.pr_uni u ++ str "}")