aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/global.mli
diff options
context:
space:
mode:
Diffstat (limited to 'library/global.mli')
-rw-r--r--library/global.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/library/global.mli b/library/global.mli
index 03469bea4..09ed4eb0a 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -19,7 +19,7 @@ val env : unit -> Environ.env
val env_is_initial : unit -> bool
-val universes : unit -> Univ.universes
+val universes : unit -> UGraph.t
val named_context_val : unit -> Environ.named_context_val
val named_context : unit -> Context.named_context