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 ++---
 kernel/uGraph.mli | 2 +-
 2 files changed, 3 insertions(+), 4 deletions(-)

(limited to 'kernel')

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
 
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 4336a22b8c..a2cc5b3116 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -86,7 +86,7 @@ val check_subtype : AUContext.t check_function
 (** {6 Dumping to a file } *)
 
 val dump_universes :
-  (constraint_type -> string -> string -> unit) -> t -> unit
+  (constraint_type -> Level.t -> Level.t -> unit) -> t -> unit
 
 (** {6 Debugging} *)
 val check_universes_invariants : t -> unit
-- 
cgit v1.2.3