aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/uGraph.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/uGraph.mli')
-rw-r--r--kernel/uGraph.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index c8ac7df5c..935a3cab4 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -17,6 +17,7 @@ type universes = t
type 'a check_function = universes -> 'a -> 'a -> bool
val check_leq : universe check_function
val check_eq : universe check_function
+val check_eq_level : universe_level check_function
(** The empty graph of universes *)
val empty_universes : universes