aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/environ.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/environ.mli')
-rw-r--r--kernel/environ.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 9f6ea522a..714c26066 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -41,7 +41,7 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool
val empty_env : env
-val universes : env -> Univ.universes
+val universes : env -> UGraph.t
val rel_context : env -> rel_context
val named_context : env -> named_context
val named_context_val : env -> named_context_val