From f53890d1629ea7aaff86ea92e5ac27ab027b2e8d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 2 Mar 2018 13:37:07 +0100
Subject: universe normalisation: put equivalence class partition in UGraph

ie don't go through having Eq constraints but directly to the unionfind.
---
 kernel/uGraph.mli | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'kernel/uGraph.mli')

diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index d4fba63fb3..cca2eb472b 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -59,7 +59,10 @@ val empty_universes : t
 
 val sort_universes : t -> t
 
-val constraints_of_universes : t -> Constraint.t
+(** [constraints_of_universes g] returns [csts] and [partition] where
+   [csts] are the non-Eq constraints and [partition] is the partition
+   of the universes into equivalence classes. *)
+val constraints_of_universes : t -> Constraint.t * LSet.t list
 
 val check_subtype : AUContext.t check_function
 (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
-- 
cgit v1.2.3