From 14c4a4281abf4d71ea33f12d8e8701ee8984e0fe Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 13 Nov 2018 15:32:06 +0100
Subject: Make UGraph printing independent of hash order

---
 kernel/uGraph.ml | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'kernel/uGraph.ml')

diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 9ff51fca55..ad94362aaf 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -942,22 +942,25 @@ let check_eq_instances g t1 t2 =
 
 (** Pretty-printing *)
 
+let pr_umap sep pr map =
+  let cmp (u,_) (v,_) = Level.compare u v in
+  Pp.prlist_with_sep sep pr (List.sort cmp (UMap.bindings map))
+
 let pr_arc prl = function
   | _, Canonical {univ=u; ltle; _} ->
     if UMap.is_empty ltle then mt ()
     else
       prl u ++ str " " ++
       v 0
-        (pr_sequence (fun (v, strict) ->
+        (pr_umap Pp.spc (fun (v, strict) ->
           (if strict then str "< " else str "<= ") ++ prl v)
-           (UMap.bindings ltle)) ++
+           ltle) ++
       fnl ()
   | u, Equiv v ->
       prl u  ++ str " = " ++ prl v ++ fnl ()
 
 let pr_universes prl g =
-  let graph = UMap.fold (fun u a l -> (u,a)::l) g.entries [] in
-  prlist (pr_arc prl) graph
+  pr_umap mt (pr_arc prl) g.entries
 
 (* Dumping constraints to a file *)
 
-- 
cgit v1.2.3


From 1310a684c8dbcbf3c94022c8e9b6cec3bf092e3d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 14 Nov 2018 13:40:00 +0100
Subject: Use universe names when printing to dot.

---
 kernel/uGraph.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'kernel/uGraph.ml')

diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index ad94362aaf..9083156745 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -967,12 +967,11 @@ let pr_universes prl g =
 let dump_universes output g =
   let dump_arc u = function
     | Canonical {univ=u; ltle; _} ->
-        let u_str = Level.to_string u in
         UMap.iter (fun v strict ->
           let typ = if strict then Lt else Le in
-          output typ u_str (Level.to_string v)) ltle;
+          output typ u v) ltle;
     | Equiv v ->
-      output Eq (Level.to_string u) (Level.to_string v)
+      output Eq u v
   in
   UMap.iter dump_arc g.entries
 
-- 
cgit v1.2.3