aboutsummaryrefslogtreecommitdiff
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, 2 insertions, 0 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 25ecdfd852..9e35e2f608 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -102,6 +102,8 @@ val rel_context : env -> Constr.rel_context
val named_context : env -> Constr.named_context
val named_context_val : env -> named_context_val
+val set_universes : UGraph.t -> env -> env
+
val opaque_tables : env -> Opaqueproof.opaquetab
val set_opaque_tables : env -> Opaqueproof.opaquetab -> env