From 051f2c1be929a46a0713b47b072bb5be0a7558d0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 24 Mar 2017 15:50:21 +0100 Subject: Fast path when checking equality of universe levels in UState. We export the relevant level equality function in UGraph which is way faster than checking that each one is smaller than the other as universes. --- kernel/uGraph.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'kernel/uGraph.mli') diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index e95cf4d1c..ed52832fa 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 -- cgit v1.2.3