aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/global.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/library/global.mli b/library/global.mli
index 2acd7e2a67..2767594171 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -22,7 +22,7 @@ val env : unit -> Environ.env
val env_is_initial : unit -> bool
val universes : unit -> UGraph.t
-val universes_lbound : unit -> Univ.Level.t
+val universes_lbound : unit -> UGraph.Bound.t
val named_context_val : unit -> Environ.named_context_val
val named_context : unit -> Constr.named_context