aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/uGraph.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/uGraph.mli')
-rw-r--r--kernel/uGraph.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index ed52832fa..935a3cab4 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -62,3 +62,6 @@ val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds
val dump_universes :
(constraint_type -> string -> string -> unit) ->
universes -> unit
+
+(** {6 Debugging} *)
+val check_universes_invariants : universes -> unit