8 files changed, 17 insertions, 12 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 244cd2865d..11d4120d7c 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -92,6 +92,8 @@ type typing_flags = {
   indices_matter: bool;
   (** The universe of an inductive type must be above that of its indices. *)
 
+  cumulative_sprop : bool;
+  (** SProp <= Type *)
 }
 
 (* some contraints are in constant_constraints, some other may be in
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 20dc21900c..b347152c16 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -26,6 +26,7 @@ let safe_flags oracle = {
   enable_VM = true;
   enable_native_compiler = true;
   indices_matter = true;
+  cumulative_sprop = false;
 }
 
 (** {6 Arities } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index de8692ff21..cf01711fe7 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -431,7 +431,7 @@ let push_subgraph (levels,csts) env =
   in
   map_universes add_subgraph env
 
-let set_engagement c env = (* Unsafe *)
+let set_engagement c env =
   { env with env_stratification =
     { env.env_stratification with env_engagement = c } }
 
@@ -445,6 +445,7 @@ let same_flags {
      share_reduction;
      enable_VM;
      enable_native_compiler;
+     cumulative_sprop;
   } alt =
   check_guarded == alt.check_guarded &&
   check_positive == alt.check_positive &&
@@ -453,14 +454,18 @@ let same_flags {
   indices_matter == alt.indices_matter &&
   share_reduction == alt.share_reduction &&
   enable_VM == alt.enable_VM &&
-  enable_native_compiler == alt.enable_native_compiler
+  enable_native_compiler == alt.enable_native_compiler &&
+  cumulative_sprop == alt.cumulative_sprop
 [@warning "+9"]
 
-let set_typing_flags c env = (* Unsafe *)
+let set_cumulative_sprop b = map_universes (UGraph.set_cumulative_sprop b)
+
+let set_typing_flags c env =
   if same_flags env.env_typing_flags c then env
-  else { env with env_typing_flags = c }
+  else set_cumulative_sprop c.cumulative_sprop { env with env_typing_flags = c }
 
-let make_sprop_cumulative = map_universes UGraph.make_sprop_cumulative
+let set_cumulative_sprop b env =
+  set_typing_flags {env.env_typing_flags with cumulative_sprop=b} env
 
 let set_allow_sprop b env =
   { env with env_stratification =
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 25ecdfd852..4195f112ca 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -310,7 +310,7 @@ 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_cumulative_sprop : bool -> env -> env
 val set_allow_sprop : bool -> env -> env
 val sprop_allowed : env -> bool
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 50922ffc52..390407fab8 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -232,8 +232,6 @@ 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
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index b42746a882..f5bd27ca12 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -135,7 +135,6 @@ val set_check_positive : bool -> safe_transformer0
 val set_check_universes : 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/uGraph.ml b/kernel/uGraph.ml
index 449cd0f0f9..5f5f0ef8cd 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -37,7 +37,7 @@ let g_map f g =
   if g.graph == g' then g
   else {g with graph=g'}
 
-let make_sprop_cumulative g = {g with sprop_cumulative=true}
+let set_cumulative_sprop b g = {g with sprop_cumulative=b}
 
 let check_smaller_expr g (u,n) (v,m) =
   let diff = n - m in
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 8a8c09e911..8d9afb0990 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -13,8 +13,8 @@ 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. *)
+val set_cumulative_sprop : bool -> t -> t
+(** Makes the system incomplete. *)
 
 type 'a check_function = t -> 'a -> 'a -> bool