2 files changed, 16 insertions, 26 deletions
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 5d7cc92181..b988ec40a7 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -222,19 +222,6 @@ let choose p g u = if Level.is_sprop u
   then if p u then Some u else None
   else G.choose p g.graph u
 
-(* Dumping constraints to a file *)
-
-let dump_universes output g =
-  let dump_arc u = function
-    | G.Node ltle ->
-      LMap.iter (fun v strict ->
-          let typ = if strict then Lt else Le in
-          output typ u v) ltle;
-    | G.Alias v ->
-      output Eq u v
-  in
-  LMap.iter dump_arc (G.repr g.graph)
-
 let check_universes_invariants g = G.check_invariants ~required_canonical:Level.is_small g.graph
 
 (** Pretty-printing *)
@@ -257,11 +244,13 @@ let pr_arc prl = let open Pp in
   | u, G.Alias v ->
     prl u  ++ str " = " ++ prl v ++ fnl ()
 
-let pr_universes prl g = pr_pmap Pp.mt (pr_arc prl) (G.repr g.graph)
+type node = G.node =
+| Alias of Level.t
+| Node of bool LMap.t
+
+let repr g = G.repr g.graph
 
-let dummy_mp = Names.DirPath.make [Names.Id.of_string "Type"]
-let make_dummy i = Level.(make (UGlobal.make dummy_mp i))
-let sort_universes g = g_map (G.sort make_dummy [Level.prop;Level.set]) g
+let pr_universes prl g = pr_pmap Pp.mt (pr_arc prl) g
 
 (** Profiling *)
 
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 87b3634e28..9ac29f5139 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -77,15 +77,9 @@ exception UndeclaredLevel of Univ.Level.t
 
 val check_declared_universes : t -> Univ.LSet.t -> unit
 
-(** {6 Pretty-printing of universes. } *)
-
-val pr_universes : (Level.t -> Pp.t) -> t -> Pp.t
-
 (** The empty graph of universes *)
 val empty_universes : t
 
-val sort_universes : t -> 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. *)
@@ -108,10 +102,17 @@ val check_subtype : lbound:Bound.t -> AUContext.t check_function
 (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
     [ctx1]. *)
 
-(** {6 Dumping to a file } *)
+(** {6 Dumping} *)
+
+type node =
+| Alias of Level.t
+| Node of bool LMap.t (** Nodes v s.t. u < v (true) or u <= v (false) *)
+
+val repr : t -> node LMap.t
+
+(** {6 Pretty-printing of universes. } *)
 
-val dump_universes :
-  (constraint_type -> Level.t -> Level.t -> unit) -> t -> unit
+val pr_universes : (Level.t -> Pp.t) -> node LMap.t -> Pp.t
 
 (** {6 Debugging} *)
 val check_universes_invariants : t -> unit