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 e95cf4d1cb..ed52832fa4 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


From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:04:58 +0200
Subject: Remove some unused values and types

---
 kernel/uGraph.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/uGraph.mli')

diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index e95cf4d1cb..c8ac7df5c6 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -61,3 +61,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
-- 
cgit v1.2.3