diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 2 |
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; |