From f821438c9759c4788d597688b25cb78f2a2c01c4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 5 Jan 2021 21:54:12 +0100
Subject: Further pushing up the printing and sorting of universes.

We expose the representation function in UGraph and change the printer
signature to work over the representation instead of the abstract type.
Similarly, the topological sorting algorithm is moved to Vernacentries.
It is now even simpler.
---
 kernel/uGraph.ml | 23 ++++++-----------------
 1 file changed, 6 insertions(+), 17 deletions(-)

(limited to 'kernel/uGraph.ml')

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 *)
 
-- 
cgit v1.2.3