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.

71 files changed, 392 insertions, 110 deletions

diff --git a/Makefile.build b/Makefile.build
index 2e4700be88..2a071fd820 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -200,7 +200,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 # the output format of the unix command time. For instance:
 #   TIME="%C (%U user, %S sys, %e total, %M maxres)"
 
-COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR) $(COQUSERFLAGS)
+COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR) $(COQUSERFLAGS) -allow-sprop
 # Beware this depends on the makefile being in a particular dir, we
 # should pass an absolute path here but windows is tricky
 # c.f. https://github.com/coq/coq/pull/9560
diff --git a/checker/checker.ml b/checker/checker.ml
index d3f346d76b..205a3984d5 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -146,6 +146,7 @@ let make_senv () =
   let senv = Safe_typing.set_engagement !impredicative_set senv in
   let senv = Safe_typing.set_indices_matter !indices_matter senv in
   let senv = Safe_typing.set_VM false senv in
+  let senv = Safe_typing.set_allow_sprop true senv in (* be smarter later *)
   Safe_typing.set_native_compiler false senv
 
 let admit_list = ref ([] : object_file list)
@@ -296,6 +297,7 @@ let explain_exn = function
       | IllFormedRecBody _ -> str"IllFormedRecBody"
       | IllTypedRecBody _ -> str"IllTypedRecBody"
       | UnsatisfiedConstraints _ -> str"UnsatisfiedConstraints"
+      | DisallowedSProp -> str"DisallowedSProp"
       | UndeclaredUniverse _ -> str"UndeclaredUniverse"))
 
   | InductiveError e ->
diff --git a/checker/values.ml b/checker/values.ml
index bcac3014be..f2b961ef56 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -95,9 +95,9 @@ let v_cons = v_tuple "constructor" [|v_ind;Int|]
 
 (** kernel/univ *)
 let v_level_global = v_tuple "Level.Global.t" [|v_dp;Int|]
-let v_raw_level = v_sum "raw_level" 2 (* Prop, Set *) 
+let v_raw_level = v_sum "raw_level" 3 (* SProp, Prop, Set *)
   [|(*Level*)[|v_level_global|]; (*Var*)[|Int|]|]
-let v_level = v_tuple "level" [|Int;v_raw_level|] 
+let v_level = v_tuple "level" [|Int;v_raw_level|]
 let v_expr = v_tuple "levelexpr" [|v_level;Int|]
 let v_univ = List v_expr
 
@@ -116,8 +116,8 @@ let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|]
 
 (** kernel/term *)
 
-let v_sort = v_sum "sort" 2 (*Prop, Set*) [|[|v_univ(*Type*)|]|]
-let v_sortfam = v_enum "sorts_family" 3
+let v_sort = v_sum "sort" 3 (*SProp, Prop, Set*) [|[|v_univ(*Type*)|]|]
+let v_sortfam = v_enum "sorts_family" 4
 
 let v_puniverses v = v_tuple "punivs" [|v;v_instance|]
 
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index a3d2f33216..5ece892aa2 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -306,6 +306,7 @@ let constr_display csr =
     incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ Level.pr u ++ fnl ())
 
   and sort_display = function
+    | SProp -> "SProp"
     | Set -> "Set"
     | Prop -> "Prop"
     | Type u -> univ_display u;
@@ -430,6 +431,7 @@ let print_pure_constr csr =
     Array.iter (fun u -> print_space (); pp (Level.pr u)) (Instance.to_array u)
 
   and sort_display = function
+    | SProp -> print_string "SProp"
     | Set -> print_string "Set"
     | Prop -> print_string "Prop"
     | Type u -> open_hbox();
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index dc30793a6e..863d930968 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -25,6 +25,7 @@ let print_vfix_app () = print_string "vfix_app"
 let print_vswith () = print_string "switch"
 
 let ppsort = function
+  | SProp -> print_string "SProp"
   | Set -> print_string "Set"
   | Prop -> print_string "Prop"
   | Type u -> print_string "Type"
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index c7b092b114..521d6b707d 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -48,6 +48,7 @@ type 'a puniverses = 'a * EInstance.t
 
 let in_punivs a = (a, EInstance.empty)
 
+let mkSProp = of_kind (Sort (ESorts.make Sorts.sprop))
 let mkProp = of_kind (Sort (ESorts.make Sorts.prop))
 let mkSet = of_kind (Sort (ESorts.make Sorts.set))
 let mkType u = of_kind (Sort (ESorts.make (Sorts.sort_of_univ u)))
@@ -81,6 +82,8 @@ let mkRef (gr,u) = let open GlobRef in match gr with
   | ConstructRef c -> mkConstructU (c,u)
   | VarRef x -> mkVar x
 
+let type1 = mkSort Sorts.type1
+
 let applist (f, arg) = mkApp (f, Array.of_list arg)
 let applistc f arg = mkApp (f, Array.of_list arg)
 
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 2f4cf7d5d0..6a144be6b3 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -104,6 +104,7 @@ val mkVar : Id.t -> t
 val mkMeta : metavariable -> t
 val mkEvar : t pexistential -> t
 val mkSort : Sorts.t -> t
+val mkSProp : t
 val mkProp : t
 val mkSet  : t
 val mkType : Univ.Universe.t -> t
@@ -128,6 +129,8 @@ val mkInt : Uint63.t -> t
 
 val mkRef : GlobRef.t * EInstance.t -> t
 
+val type1 : t
+
 val applist : t * t list -> t
 val applistc : t -> t list -> t
 
diff --git a/engine/evd.ml b/engine/evd.ml
index b8c52b27df..b89222cf8e 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -962,7 +962,7 @@ let normalize_universe_instance evd l =
 
 let normalize_sort evars s =
   match s with
-  | Prop | Set -> s
+  | SProp | Prop | Set -> s
   | Type u -> 
     let u' = normalize_universe evars u in
     if u' == u then s else Sorts.sort_of_univ u'
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 7ef4108c22..46fdf08e10 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -136,6 +136,7 @@ let lowercase_first_char id = (* First character of a constr *)
         s ^ Unicode.lowercase_first_char s'
 
 let sort_hdchar = function
+  | SProp -> "P"
   | Prop -> "P"
   | Set -> "S"
   | Type _ -> "T"
diff --git a/engine/termops.ml b/engine/termops.ml
index 2f766afaa6..9c4b64b60d 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1098,7 +1098,8 @@ let is_template_polymorphic_ind env sigma f =
 
 let base_sort_cmp pb s0 s1 =
   match (s0,s1) with
-  | Prop, Prop | Set, Set | Type _, Type _ -> true
+  | SProp, SProp | Prop, Prop | Set, Set | Type _, Type _ -> true
+  | SProp, _ | _, SProp -> false
   | Prop, Set | Prop, Type _ | Set, Type _ -> pb == Reduction.CUMUL
   | Set, Prop | Type _, Prop | Type _, Set -> false
 
diff --git a/engine/uState.ml b/engine/uState.ml
index 77d1896683..6f4f40e2c5 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -37,18 +37,25 @@ type t =
    uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *)
    uctx_weak_constraints : UPairSet.t
  }
-  
+
+let initial_sprop_cumulative = UGraph.make_sprop_cumulative UGraph.initial_universes
+
 let empty =
   { uctx_names = UNameMap.empty, LMap.empty;
     uctx_local = ContextSet.empty;
     uctx_seff_univs = LSet.empty;
     uctx_univ_variables = LMap.empty;
     uctx_univ_algebraic = LSet.empty;
-    uctx_universes = UGraph.initial_universes;
-    uctx_initial_universes = UGraph.initial_universes;
+    uctx_universes = initial_sprop_cumulative;
+    uctx_initial_universes = initial_sprop_cumulative;
     uctx_weak_constraints = UPairSet.empty; }
 
+let elaboration_sprop_cumul =
+  Goptions.declare_bool_option_and_ref ~depr:false ~name:"SProp cumulativity during elaboration"
+    ~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true
+
 let make u =
+  let u = if elaboration_sprop_cumul () then UGraph.make_sprop_cumulative u else u in
     { empty with 
       uctx_universes = u; uctx_initial_universes = u}
 
@@ -710,7 +717,7 @@ let universe_of_name uctx s =
   UNameMap.find s (fst uctx.uctx_names)
 
 let update_sigma_env uctx env =
-  let univs = Environ.universes env in
+  let univs = UGraph.make_sprop_cumulative (Environ.universes env) in
   let eunivs =
     { uctx with uctx_initial_universes = univs;
                          uctx_universes = univs }
diff --git a/engine/univGen.ml b/engine/univGen.ml
index 4ad7fccb3a..c310331b15 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -128,6 +128,7 @@ let type_of_reference env r =
 let type_of_global t = type_of_reference (Global.env ()) t
 
 let fresh_sort_in_family = function
+  | InSProp -> Sorts.sprop, ContextSet.empty
   | InProp -> Sorts.prop, ContextSet.empty
   | InSet -> Sorts.set, ContextSet.empty
   | InType ->
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index 1619ac3d34..46ff6340b4 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -268,6 +268,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
 module UPairs = OrderedType.UnorderedPair(Univ.Level)
 module UPairSet = Set.Make (UPairs)
 
+(* TODO check is_small/sprop *)
 let normalize_context_set g ctx us algs weak =
   let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
   (* Keep the Prop/Set <= i constraints separate for minimization *)
@@ -275,7 +276,7 @@ let normalize_context_set g ctx us algs weak =
     Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts
   in
   let smallles = if get_set_minimization ()
-    then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx) smallles
+    then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx && not (Level.is_sprop l)) smallles
     else Constraint.empty
   in
   let csts, partition =
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 8e49800982..d5cb25d1fb 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -755,6 +755,7 @@ let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_lo
 (* mapping glob_constr to constr_expr                                    *)
 
 let extern_glob_sort = function
+  | GSProp -> GSProp
   | GProp -> GProp
   | GSet -> GSet
   | GType _ as s when !print_universes -> s
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7f1dc70d95..b4c570d444 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1020,6 +1020,7 @@ let sort_info_of_level_info (info: level_info) : (Libnames.qualid * int) option
 
 let glob_sort_of_level (level: glob_level) : glob_sort =
   match level with
+  | GSProp -> GSProp
   | GProp -> GProp
   | GSet -> GSet
   | GType info -> GType [sort_info_of_level_info info]
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 "}")
diff --git a/library/global.ml b/library/global.ml
index cf996ce644..d9f8a6ffa3 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -90,6 +90,9 @@ let set_engagement c = globalize0 (Safe_typing.set_engagement c)
 let set_indices_matter b = globalize0 (Safe_typing.set_indices_matter b)
 let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
 let typing_flags () = Environ.typing_flags (env ())
+let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative
+let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b)
+let sprop_allowed () = Environ.sprop_allowed (env())
 let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd)
 let add_constant ~in_section id d = globalize (Safe_typing.add_constant ~in_section (i2l id) d)
 let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie)
diff --git a/library/global.mli b/library/global.mli
index afb017a905..ca88d2dafd 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -32,6 +32,9 @@ val set_engagement : Declarations.engagement -> unit
 val set_indices_matter : bool -> unit
 val set_typing_flags : Declarations.typing_flags -> unit
 val typing_flags : unit -> Declarations.typing_flags
+val make_sprop_cumulative : unit -> unit
+val set_allow_sprop : bool -> unit
+val sprop_allowed : unit -> bool
 
 (** Variables, Local definitions, constants, inductive types *)
 
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index b3ae24e941..6f73a3e4ed 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -31,7 +31,7 @@ let ldots_var = Id.of_string ".."
 let constr_kw =
   [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for";
     "end"; "as"; "let"; "if"; "then"; "else"; "return";
-    "Prop"; "Set"; "Type"; ".("; "_"; "..";
+    "SProp"; "Prop"; "Set"; "Type"; ".("; "_"; "..";
     "`{"; "`("; "{|"; "|}" ]
 
 let _ = List.iter CLexer.add_keyword constr_kw
@@ -153,6 +153,7 @@ GRAMMAR EXTEND Gram
   sort:
     [ [ "Set"  -> { GSet }
       | "Prop" -> { GProp }
+      | "SProp" -> { GSProp }
       | "Type" -> { GType [] }
       | "Type"; "@{"; u = universe; "}" -> { GType u }
       ] ]
@@ -160,6 +161,7 @@ GRAMMAR EXTEND Gram
   sort_family:
     [ [ "Set"  -> { Sorts.InSet }
       | "Prop" -> { Sorts.InProp }
+      | "SProp" -> { Sorts.InSProp }
       | "Type" -> { Sorts.InType }
       ] ]
   ;
@@ -323,6 +325,7 @@ GRAMMAR EXTEND Gram
   ;
   universe_level:
     [ [ "Set" -> { GSet }
+      (* no parsing SProp as a level *)
       | "Prop" -> { GProp }
       | "Type" -> { GType UUnknown }
       | "_" -> { GType UAnonymous }
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index ef6c07bff2..877ea9a537 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -73,13 +73,18 @@ type flag = info * scheme
 (*s [flag_of_type] transforms a type [t] into a [flag].
   Really important function. *)
 
+let info_of_family = function
+  | InSProp | InProp -> Logic
+  | InSet | InType -> Info
+
+let info_of_sort s = info_of_family (Sorts.family s)
+
 let rec flag_of_type env sg t : flag =
   let t = whd_all env sg t in
   match EConstr.kind sg t with
     | Prod (x,t,c) -> flag_of_type (EConstr.push_rel (LocalAssum (x,t)) env) sg c
-    | Sort s when Sorts.is_prop (EConstr.ESorts.kind sg s) -> (Logic,TypeScheme)
-    | Sort _ -> (Info,TypeScheme)
-    | _ -> if (sort_of env sg t) == InProp then (Logic,Default) else (Info,Default)
+    | Sort s -> (info_of_sort (EConstr.ESorts.kind sg s),TypeScheme)
+    | _ -> (info_of_family (sort_of env sg t),Default)
 
 (*s Two particular cases of [flag_of_type]. *)
 
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 42dc66dcf4..98d369aeda 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -49,7 +49,8 @@ let functional_induction with_clean c princl pat =
 		    user_err  (str "Cannot find induction information on "++
                                        Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') )
 		in
-		match Tacticals.elimination_sort_of_goal g with
+                match Tacticals.elimination_sort_of_goal g with
+                | InSProp -> finfo.sprop_lemma
 		| InProp -> finfo.prop_lemma
 		| InSet -> finfo.rec_lemma
 		| InType -> finfo.rect_lemma
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index cba3cc3d42..88546e9ae8 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -199,6 +199,7 @@ type function_info =
       rect_lemma : Constant.t option;
       rec_lemma : Constant.t option;
       prop_lemma : Constant.t option;
+      sprop_lemma : Constant.t option;
       is_general : bool; (* Has this function been defined using general recursive definition *)
     }
 
@@ -249,6 +250,7 @@ let subst_Function (subst,finfos) =
   let rect_lemma' = Option.Smart.map do_subst_con finfos.rect_lemma in
   let rec_lemma' = Option.Smart.map do_subst_con finfos.rec_lemma in
   let prop_lemma' =  Option.Smart.map do_subst_con finfos.prop_lemma in
+  let sprop_lemma' = Option.Smart.map do_subst_con finfos.sprop_lemma in
   if function_constant' == finfos.function_constant &&
     graph_ind' == finfos.graph_ind &&
     equation_lemma' == finfos.equation_lemma &&
@@ -256,7 +258,8 @@ let subst_Function (subst,finfos) =
     completeness_lemma' == finfos.completeness_lemma &&
     rect_lemma' == finfos.rect_lemma &&
     rec_lemma' == finfos.rec_lemma &&
-    prop_lemma' == finfos.prop_lemma
+    prop_lemma' == finfos.prop_lemma &&
+    sprop_lemma' == finfos.sprop_lemma
   then finfos
   else
     { function_constant = function_constant';
@@ -267,6 +270,7 @@ let subst_Function (subst,finfos) =
       rect_lemma = rect_lemma' ;
       rec_lemma = rec_lemma';
       prop_lemma = prop_lemma';
+      sprop_lemma = sprop_lemma';
       is_general = finfos.is_general
     }
 
@@ -333,6 +337,7 @@ let add_Function is_general f =
   and rect_lemma = find_or_none (Nameops.add_suffix f_id "_rect")
   and rec_lemma = find_or_none (Nameops.add_suffix f_id "_rec")
   and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind")
+  and sprop_lemma = find_or_none (Nameops.add_suffix f_id "_sind")
   and graph_ind =
     match Nametab.locate (qualid_of_ident (mk_rel_id f_id))
     with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive.")
@@ -345,6 +350,7 @@ let add_Function is_general f =
       rect_lemma = rect_lemma;
       rec_lemma = rec_lemma;
       prop_lemma = prop_lemma;
+      sprop_lemma = sprop_lemma;
       graph_ind = graph_ind;
       is_general = is_general
 
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 1e0b95df34..102994f61e 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -70,6 +70,7 @@ type function_info =
       rect_lemma : Constant.t option;
       rec_lemma : Constant.t option;
       prop_lemma : Constant.t option;
+      sprop_lemma : Constant.t option;
       is_general : bool;
     }
 
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 026c00b849..fcab98c7e8 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -199,7 +199,8 @@ let id_of_name = function
 	  basename
        | Sort s ->
           begin
-	    match ESorts.kind sigma s with
+            match ESorts.kind sigma s with
+            | Sorts.SProp -> Label.to_id (Label.make "SProp")
             | Sorts.Prop -> Label.to_id (Label.make "Prop")
             | Sorts.Set -> Label.to_id (Label.make "Set")
             | Sorts.Type _ -> Label.to_id (Label.make "Type")
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 0e6aaaa408..aa3fbc4577 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -398,7 +398,7 @@ let inh_app_fun_core ~program_mode env evd j =
     match EConstr.kind evd t with
     | Prod (_,_,_) -> (evd,j)
     | Evar ev ->
-	let (evd',t) = Evardefine.define_evar_as_product evd ev in
+        let (evd',t) = Evardefine.define_evar_as_product env evd ev in
 	  (evd',{ uj_val = j.uj_val; uj_type = t })
     | _ ->
       	try let t,p =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 99cd89cc2a..48e4b5414e 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -597,6 +597,7 @@ let detype_universe sigma u =
   Univ.Universe.map fn u
 
 let detype_sort sigma = function
+  | SProp -> GSProp
   | Prop -> GProp
   | Set -> GSet
   | Type u ->
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 55dfdc0574..799a81cf4b 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -72,7 +72,7 @@ let idx = Namegen.default_dependent_ident
 
 (* Refining an evar to a product *)
 
-let define_pure_evar_as_product evd evk =
+let define_pure_evar_as_product env evd evk =
   let open Context.Named.Declaration in
   let evi = Evd.find_undefined evd evk in
   let evenv = evar_env evi in
@@ -88,7 +88,7 @@ let define_pure_evar_as_product evd evk =
     let newenv = push_named (LocalAssum (id, dom)) evenv in
     let src = subterm_source evk ~where:Codomain evksrc in
     let filter = Filter.extend 1 (evar_filter evi) in
-      if Sorts.is_prop (ESorts.kind evd1 s) then
+      if Environ.is_impredicative_sort env (ESorts.kind evd1 s) then
        (* Impredicative product, conclusion must fall in [Prop]. *)
         new_evar newenv evd1 concl ~src ~filter
       else
@@ -106,8 +106,8 @@ let define_pure_evar_as_product evd evk =
 
 (* Refine an applied evar to a product and returns its instantiation *)
 
-let define_evar_as_product evd (evk,args) =
-  let evd,prod = define_pure_evar_as_product evd evk in
+let define_evar_as_product env evd (evk,args) =
+  let evd,prod = define_pure_evar_as_product env evd evk in
   (* Quick way to compute the instantiation of evk with args *)
   let na,dom,rng = destProd evd prod in
   let evdom = mkEvar (fst (destEvar evd dom), args) in
@@ -131,7 +131,7 @@ let define_pure_evar_as_lambda env evd evk =
   let typ = Reductionops.whd_all evenv evd (evar_concl evi) in
   let evd1,(na,dom,rng) = match EConstr.kind evd typ with
   | Prod (na,dom,rng) -> (evd,(na,dom,rng))
-  | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd evd typ
+  | Evar ev' -> let evd,typ = define_evar_as_product env evd ev' in evd,destProd evd typ
   | _ -> error_not_product env evd typ in
   let avoid = Environ.ids_of_named_context_val evi.evar_hyps in
   let id =
@@ -182,10 +182,10 @@ let split_tycon ?loc env evd tycon =
       match EConstr.kind evd t with
 	| Prod (na,dom,rng) -> evd, (na, dom, rng)
 	| Evar ev (* ev is undefined because of whd_all *) ->
-	    let (evd',prod) = define_evar_as_product evd ev in
+            let (evd',prod) = define_evar_as_product env evd ev in
 	    let (_,dom,rng) = destProd evd prod in
 	      evd',(Anonymous, dom, rng)
-	| App (c,args) when isEvar evd c ->
+        | App (c,args) when isEvar evd c ->
 	    let (evd',lam) = define_evar_as_lambda env evd (destEvar evd c) in
 	    real_split evd' (mkApp (lam,args))
 	| _ -> error_not_product ?loc env evd c
diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli
index cd23f9c601..7b5ced49bf 100644
--- a/pretyping/evardefine.mli
+++ b/pretyping/evardefine.mli
@@ -38,7 +38,7 @@ val split_tycon :
 val valcon_of_tycon : type_constraint -> val_constraint
 val lift_tycon : int -> type_constraint -> type_constraint
 
-val define_evar_as_product : evar_map -> existential -> evar_map * types
+val define_evar_as_product : env -> evar_map -> existential -> evar_map * types
 val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types
 val define_evar_as_sort : env -> evar_map -> existential -> evar_map * Sorts.t
 
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 8670c1d964..c57cf88cc6 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -24,6 +24,7 @@ type existential_name = Id.t
 (** Sorts *)
 
 type 'a glob_sort_gen =
+  | GSProp (** representation of [SProp] literal *)
   | GProp (** representation of [Prop] literal *)
   | GSet  (** representation of [Set] literal *)
   | GType of 'a (** representation of [Type] literal *)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index bd321d5886..a9b419f03f 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -588,6 +588,7 @@ let build_induction_scheme env sigma pind dep kind =
 (*s Eliminations. *)
 
 let elimination_suffix = function
+  | InSProp -> "_sind"
   | InProp -> "_ind"
   | InSet  -> "_rec"
   | InType -> "_rect"
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 6803ea7d9b..305ebf3dd5 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -153,6 +153,7 @@ let pattern_of_constr env sigma t =
     | Rel n  -> PRel n
     | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n)))
     | Var id -> PVar id
+    | Sort SProp -> PSort GSProp
     | Sort Prop -> PSort GProp
     | Sort Set -> PSort GSet
     | Sort (Type _) -> PSort (GType [])
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 =
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index a0d459fe6b..82926ba280 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -67,6 +67,7 @@ type pretype_error =
   | UnsatisfiableConstraints of
     (Evar.t * Evar_kinds.t) option * Evar.Set.t option
     (** unresolvable evar, connex component *)
+  | DisallowedSProp
 
 exception PretypeError of env * Evd.evar_map * pretype_error
 
@@ -158,6 +159,8 @@ val error_var_not_found : ?loc:Loc.t -> env -> Evd.evar_map -> Id.t -> 'b
 
 val error_evar_not_found : ?loc:Loc.t -> env -> Evd.evar_map -> Id.t -> 'b
 
+val error_disallowed_sprop : env -> Evd.evar_map -> 'a
+
 (** {6 Typeclass errors } *)
 
 val unsatisfiable_constraints : env -> Evd.evar_map -> Evar.t option ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index ae1b4af3c3..62dd50d934 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -398,11 +398,13 @@ let pretype_id pretype k0 loc env sigma id =
 (* Main pretyping function                                               *)
 
 let interp_known_glob_level ?loc evd = function
+  | GSProp -> Univ.Level.sprop
   | GProp -> Univ.Level.prop
   | GSet -> Univ.Level.set
   | GType s -> interp_known_level_info ?loc evd s
 
 let interp_glob_level ?loc evd : glob_level -> _ = function
+  | GSProp -> evd, Univ.Level.sprop
   | GProp -> evd, Univ.Level.prop
   | GSet -> evd, Univ.Level.set
   | GType s -> interp_level_info ?loc evd s
@@ -452,6 +454,7 @@ let judge_of_Type ?loc evd s =
     evd, judge
 
 let pretype_sort ?loc sigma = function
+  | GSProp -> sigma, judge_of_sprop
   | GProp -> sigma, judge_of_prop
   | GSet -> sigma, judge_of_set
   | GType s -> judge_of_Type ?loc sigma s
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index fd3c77338c..1ca9e6590d 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -150,7 +150,7 @@ let retype ?(polyprop=true) sigma =
     | Cast (c,_, s) when isSort sigma s -> destSort sigma s
     | Sort s ->
       begin match ESorts.kind sigma s with
-      | Prop | Set -> Sorts.type1
+      | SProp | Prop | Set -> Sorts.type1
       | Type u -> Sorts.sort_of_univ (Univ.super u)
       end
     | Prod (name,t,c2) ->
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index ea6e52e1f8..ed020e243d 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -65,7 +65,7 @@ let judge_of_applied_inductive_knowing_parameters env sigma funj ind argjv =
          match EConstr.kind sigma (whd_all env sigma typ) with
          | Prod (_,c1,c2) -> sigma, (c1,c2)
          | Evar ev ->
-             let (sigma,t) = Evardefine.define_evar_as_product sigma ev in
+             let (sigma,t) = Evardefine.define_evar_as_product env sigma ev in
              let (_,c1,c2) = destProd sigma t in
              sigma, (c1,c2)
          | _ ->
@@ -90,7 +90,7 @@ let judge_of_apply env sigma funj argjv =
          match EConstr.kind sigma (whd_all env sigma typ) with
          | Prod (_,c1,c2) -> sigma, (c1,c2)
          | Evar ev ->
-             let (sigma,t) = Evardefine.define_evar_as_product sigma ev in
+             let (sigma,t) = Evardefine.define_evar_as_product env sigma ev in
              let (_,c1,c2) = destProd sigma t in
              sigma, (c1,c2)
          | _ ->
@@ -230,6 +230,10 @@ let check_cofix env sigma pcofix =
 
 (* The typing machine with universes and existential variables. *)
 
+let judge_of_sprop =
+  { uj_val = EConstr.mkSProp;
+    uj_type = EConstr.type1 }
+
 let judge_of_prop =
   { uj_val = EConstr.mkProp;
     uj_type = EConstr.mkSort Sorts.type1 }
@@ -361,6 +365,9 @@ let rec execute env sigma cstr =
 
     | Sort s ->
       begin match ESorts.kind sigma s with
+        | SProp ->
+          if Environ.sprop_allowed env then sigma, judge_of_sprop
+          else error_disallowed_sprop env sigma
         | Prop -> sigma, judge_of_prop
         | Set -> sigma, judge_of_set
         | Type u -> sigma, judge_of_type u
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 1ea16bbf34..9bd369a155 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -46,6 +46,7 @@ val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr ->
 val check_type_fixpoint : ?loc:Loc.t -> env -> evar_map ->
   Names.Name.t array -> types array -> unsafe_judgment array -> evar_map
 
+val judge_of_sprop : unsafe_judgment
 val judge_of_prop : unsafe_judgment
 val judge_of_set : unsafe_judgment
 val judge_of_apply : env -> evar_map -> unsafe_judgment -> unsafe_judgment array ->
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 26202ef4ca..ad2b51b23d 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -169,12 +169,14 @@ let tag_var = tag Tag.variable
   let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
 
   let pr_glob_sort = let open Glob_term in function
+    | GSProp -> tag_type (str "SProp")
     | GProp -> tag_type (str "Prop")
     | GSet -> tag_type (str "Set")
     | GType [] -> tag_type (str "Type")
     | GType u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u)
 
   let pr_glob_level = let open Glob_term in function
+    | GSProp -> tag_type (str "SProp")
     | GProp -> tag_type (str "Prop")
     | GSet -> tag_type (str "Set")
     | GType UUnknown -> tag_type (str "Type")
@@ -197,6 +199,8 @@ let tag_var = tag Tag.variable
   let pr_patvar = pr_id
 
   let pr_glob_sort_instance = let open Glob_term in function
+    | GSProp ->
+      tag_type (str "SProp")
     | GProp ->
       tag_type (str "Prop")
     | GSet ->
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 5dd55b8a9f..554fe3cbed 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -66,7 +66,7 @@ module RelDecl = Context.Rel.Declaration
 
 let hid = Id.of_string "H"
 let xid = Id.of_string "X"
-let default_id_of_sort = function InProp | InSet -> hid | InType -> xid
+let default_id_of_sort = function InSProp | InProp | InSet -> hid | InType -> xid
 let fresh env id = next_global_ident_away id Id.Set.empty
 let with_context_set ctx (b, ctx') = 
   (b, Univ.ContextSet.union ctx ctx')
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 415225454a..ee9d117d4d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -947,7 +947,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
         let name = find_name false (LocalDef (name,b,t)) name_flag gl in
 	build_intro_tac name move_flag tac
     | Evar ev when force_flag ->
-        let sigma, t = Evardefine.define_evar_as_product sigma ev in
+        let sigma, t = Evardefine.define_evar_as_product env sigma ev in
         Tacticals.New.tclTHEN
           (Proofview.Unsafe.tclEVARS sigma)
           (intro_then_gen name_flag move_flag force_flag dep_flag tac)
diff --git a/test-suite/bugs/closed/bug_3325.v b/test-suite/bugs/closed/bug_3325.v
index 36c065ebe8..835b8a7f33 100644
--- a/test-suite/bugs/closed/bug_3325.v
+++ b/test-suite/bugs/closed/bug_3325.v
@@ -1,13 +1,13 @@
 Typeclasses eauto := debug.
 Set Printing All.
 
-Axiom SProp : Set.
-Axiom sp : SProp.
+Axiom sProp : Set.
+Axiom sp : sProp.
 
 (* If we hardcode valueType := nat, it goes through *)
 Class StateIs := {
   valueType : Type;
-  stateIs : valueType -> SProp
+  stateIs : valueType -> sProp
 }.
 
 Instance NatStateIs : StateIs := {
@@ -17,17 +17,17 @@ Instance NatStateIs : StateIs := {
 Canonical Structure NatStateIs.
 
 Class LogicOps F := { land: F -> F }.
-Instance : LogicOps SProp. Admitted.
+Instance : LogicOps sProp. Admitted.
 Instance : LogicOps Prop. Admitted.
 
 Parameter (n : nat).
 (* If this is a [Definition], the resolution goes through fine. *)
 Notation vn := (@stateIs _ n).
 Definition vn' := (@stateIs _ n).
-Definition GOOD : SProp :=
+Definition GOOD : sProp :=
   @land _ _ vn'.
 (* This doesn't resolve, if PropLogicOps is defined later than SPropLogicOps *)
-Definition BAD : SProp :=
+Definition BAD : sProp :=
   @land _ _ vn.
 
 
diff --git a/test-suite/bugs/closed/bug_sprop_14.v b/test-suite/bugs/closed/bug_sprop_14.v
new file mode 100644
index 0000000000..1e6e9b30de
--- /dev/null
+++ b/test-suite/bugs/closed/bug_sprop_14.v
@@ -0,0 +1,26 @@
+(* -*- coq-prog-args: ("-allow-sprop"); -*- *)
+
+Set Universe Polymorphism.
+
+Inductive False : SProp :=.
+
+Axiom ℙ@{} : SProp.
+
+Definition TYPE@{i} := ℙ -> Type@{i}.
+Definition PROP@{} := ℙ -> SProp.
+
+Definition El@{i} (A : TYPE@{i}) := forall p, A p.
+Definition sEl@{} (A : PROP@{}) : SProp := forall p, A p.
+
+Definition SPropᶠ@{} := fun (p : ℙ) => SProp.
+
+Definition sProdᶠ@{i}
+  (A : TYPE@{i})
+  (B : forall (p : ℙ), El A -> SProp) : PROP := fun (p : ℙ) => forall x : El A, B p x.
+
+Definition Falseᶠ : El SPropᶠ := fun p => False.
+
+Definition EMᶠ : sEl (sProdᶠ SPropᶠ (fun p A => ((sProdᶠ A (fun p _ => Falseᶠ p))) p)).
+Proof.
+Fail Admitted.
+Abort.
diff --git a/test-suite/success/sprop.v b/test-suite/success/sprop.v
new file mode 100644
index 0000000000..1e17d090c2
--- /dev/null
+++ b/test-suite/success/sprop.v
@@ -0,0 +1,19 @@
+(* -*- mode: coq; coq-prog-args: ("-allow-sprop") -*- *)
+
+Check SProp.
+
+Definition iUnit : SProp := forall A : SProp, A -> A.
+Definition itt : iUnit := fun A a => a.
+
+Definition iSquash (A:Type) : SProp
+  := forall P : SProp, (A -> P) -> P.
+Definition isquash A : A -> iSquash A
+  := fun a P f => f a.
+
+Fail Check (fun A : SProp => A : Type).
+
+Lemma foo : Prop.
+Proof. pose (fun A : SProp => A : Type). Abort.
+
+(* define evar as product *)
+Check (fun (f:(_:SProp)) => f _).
diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
index 98368d76ca..fa8b771a74 100644
--- a/tools/coq_dune.ml
+++ b/tools/coq_dune.ml
@@ -127,6 +127,7 @@ module Options = struct
   let all_opts =
   [ { enabled = false; cmd = "-debug"; }
   ; { enabled = false; cmd = "-native_compiler"; }
+  ; { enabled = true; cmd = "-allow-sprop"; }
   ]
 
   let build_coq_flags () =
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index bbccae8edb..d682d3641f 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -60,6 +60,8 @@ type t = {
   indices_matter : bool;
   enable_VM : bool;
   native_compiler : native_compiler;
+  allow_sprop : bool;
+  cumulative_sprop : bool;
 
   stm_flags   : Stm.AsyncOpts.stm_opt;
   debug       : bool;
@@ -110,6 +112,8 @@ let default = {
   indices_matter = false;
   enable_VM = true;
   native_compiler = default_native;
+  allow_sprop = false;
+  cumulative_sprop = false;
 
   stm_flags    = Stm.AsyncOpts.default_opts;
   debug        = false;
@@ -477,6 +481,9 @@ let parse_args ~help ~init arglist : t * string list =
     |"-filteropts" -> { oval with filter_opts = true }
     |"-impredicative-set" ->
       { oval with impredicative_set = Declarations.ImpredicativeSet }
+    |"-allow-sprop" -> { oval with allow_sprop = true }
+    |"-disallow-sprop" -> { oval with allow_sprop = false }
+    |"-sprop-cumulative" -> { oval with cumulative_sprop = true }
     |"-indices-matter" -> { oval with indices_matter = true }
     |"-m"|"--memory" -> { oval with memory_stat = true }
     |"-noinit"|"-nois" -> { oval with load_init = false }
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index b89a88d1f6..97a62e97e4 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -35,6 +35,8 @@ type t = {
   indices_matter : bool;
   enable_VM : bool;
   native_compiler : native_compiler;
+  allow_sprop : bool;
+  cumulative_sprop : bool;
 
   stm_flags   : Stm.AsyncOpts.stm_opt;
   debug       : bool;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 92ac200bc0..f7fb26fe3a 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -189,6 +189,8 @@ let init_toplevel ~help ~init custom_init arglist =
   Global.set_indices_matter opts.indices_matter;
   Global.set_VM opts.enable_VM;
   Global.set_native_compiler (match opts.native_compiler with NativeOff -> false | NativeOn _ -> true);
+  Global.set_allow_sprop opts.allow_sprop;
+  if opts.cumulative_sprop then Global.make_sprop_cumulative ();
 
   (* Allow the user to load an arbitrary state here *)
   inputstate opts;
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 94ec6bb70d..513374c2af 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -69,6 +69,8 @@ let print_usage_common co command =
 \n  -noglob                do not dump globalizations\
 \n  -dump-glob f           dump globalizations in file f (to be used by coqdoc)\
 \n  -impredicative-set     set sort Set impredicative\
+\n  -allow-sprop           allow using the proof irrelevant SProp sort\
+\n  -sprop-cumulative      make sort SProp cumulative with the rest of the hierarchy\
 \n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
 \n  -type-in-type          disable universe consistency checking\
 \n  -mangle-names x        mangle auto-generated names using prefix x\
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 2ef2317d86..fd5970e8ca 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -710,6 +710,9 @@ let explain_undeclared_universe env sigma l =
     Termops.pr_evd_level sigma l ++
     spc () ++ str "(maybe a bugged tactic)."
 
+let explain_disallowed_sprop () =
+  Pp.(str "SProp not allowed, you need to use -allow-sprop.")
+
 let explain_type_error env sigma err =
   let env = make_all_name_different env sigma in
   match err with
@@ -751,6 +754,7 @@ let explain_type_error env sigma err =
       explain_unsatisfied_constraints env sigma cst
   | UndeclaredUniverse l ->
      explain_undeclared_universe env sigma l
+  | DisallowedSProp -> explain_disallowed_sprop ()
 
 let pr_position (cl,pos) =
   let clpos = match cl with
@@ -864,6 +868,7 @@ let explain_pretype_error env sigma err =
   | TypingError t -> explain_type_error env sigma t
   | CannotUnifyOccurrences (b,c1,c2,e) -> explain_cannot_unify_occurrences env sigma b c1 c2 e
   | UnsatisfiableConstraints (c,comp) -> explain_unsatisfiable_constraints env sigma c comp
+  | DisallowedSProp -> explain_disallowed_sprop ()
 
 (* Module errors *)
 
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index caafd6ac2f..28ee3d184f 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -246,6 +246,9 @@ let declare_one_induction_scheme ind =
   let from_prop = kind == InProp in
   let depelim = Inductiveops.has_dependent_elim mib in
   let kelim = elim_sorts (mib,mip) in
+  let kelim = if Global.sprop_allowed () then kelim
+    else List.filter (fun s -> s <> InSProp) kelim
+  in
   let elims =
     List.map_filter (fun (sort,kind) ->
       if Sorts.List.mem sort kelim then Some kind else None)
@@ -347,19 +350,23 @@ requested
           match sort_of_ind with
           | InProp ->
               if isdep then (match z with
+              | InSProp -> inds ^ "s_dep"
               | InProp -> inds ^ "_dep"
               | InSet  -> recs ^ "_dep"
               | InType -> recs ^ "t_dep")
               else ( match z with
+              | InSProp -> inds ^ "s"
               | InProp -> inds
               | InSet -> recs
               | InType -> recs ^ "t" )
           | _ ->
               if isdep then (match z with
+              | InSProp -> inds ^ "s"
               | InProp -> inds
               | InSet -> recs
               | InType -> recs ^ "t" )
               else (match z with
+              | InSProp -> inds ^ "s_nodep"
               | InProp -> inds ^ "_nodep"
               | InSet -> recs ^ "_nodep"
               | InType -> recs ^ "t_nodep")