Merge PR #12313: Make explicit that UGraph lower bounds are only of two kinds.

Reviewed-by: SkySkimmer

1 files changed, 2 insertions, 2 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index d6d52dbc2b..182ed55d0e 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -67,7 +67,7 @@ end
 type stratification = {
   env_universes : UGraph.t;
   env_sprop_allowed : bool;
-  env_universes_lbound : Univ.Level.t;
+  env_universes_lbound : UGraph.Bound.t;
   env_engagement : engagement
 }
 
@@ -129,7 +129,7 @@ let empty_env = {
   env_stratification = {
     env_universes = UGraph.initial_universes;
     env_sprop_allowed = true;
-    env_universes_lbound = Univ.Level.set;
+    env_universes_lbound = UGraph.Bound.Set;
     env_engagement = PredicativeSet };
   env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
   retroknowledge = Retroknowledge.empty;