aboutsummaryrefslogtreecommitdiff
path: root/kernel/environ.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/environ.mli')
-rw-r--r--kernel/environ.mli6
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 7a46538772..79e632daa0 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -62,7 +62,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
}
@@ -96,8 +96,8 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool
val empty_env : env
val universes : env -> UGraph.t
-val universes_lbound : env -> Univ.Level.t
-val set_universes_lbound : env -> Univ.Level.t -> env
+val universes_lbound : env -> UGraph.Bound.t
+val set_universes_lbound : env -> UGraph.Bound.t -> env
val rel_context : env -> Constr.rel_context
val named_context : env -> Constr.named_context
val named_context_val : env -> named_context_val