Merge PR #11997: Clean and fix definitions of options.

Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: jfehrle

1 files changed, 1 insertions, 1 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 2d2c9a454b..de8692ff21 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -128,7 +128,7 @@ let empty_env = {
   env_nb_rel = 0;
   env_stratification = {
     env_universes = UGraph.initial_universes;
-    env_sprop_allowed = false;
+    env_sprop_allowed = true;
     env_universes_lbound = Univ.Level.set;
     env_engagement = PredicativeSet };
   env_typing_flags = Declareops.safe_flags Conv_oracle.empty;