Merge PR #7324: Infrastructure for ocamldebug on the checker

2 files changed, 18 insertions, 2 deletions

diff --git a/checker/univ.ml b/checker/univ.ml
index fc07640774..7d285b6feb 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -142,7 +142,13 @@ end
 
 (** Level sets and maps *)
 module LMap = HMap.Make (Level)
-module LSet = LMap.Set
+module LSet = struct
+  include LMap.Set
+
+  let pr s =
+    str"{" ++ prlist_with_sep spc Level.pr (elements s) ++ str"}"
+
+end
 
 type 'a universe_map = 'a LMap.t
 
diff --git a/checker/univ.mli b/checker/univ.mli
index 935f0a2b8d..6cd3b36382 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -49,6 +49,7 @@ sig
   val make : Level.t -> t
   (** Create a universe representing the given level. *)
 
+  val pr : t -> Pp.t
 end
 
 type universe = Universe.t
@@ -140,7 +141,14 @@ val check_constraints : constraints -> universes -> bool
 
 (** Polymorphic maps from universe levels to 'a *)
 module LMap : CSig.MapS with type key = universe_level
-module LSet : CSig.SetS with type elt = universe_level
+module LSet :
+sig
+  include CSig.SetS with type elt = Level.t
+
+  val pr : t -> Pp.t
+  (** Pretty-printing *)
+end
+
 type 'a universe_map = 'a LMap.t
 
 (** {6 Substitution} *)
@@ -216,6 +224,8 @@ sig
   val instantiate : Instance.t -> t -> Constraint.t
   val repr : t -> UContext.t
 
+  val pr : (Level.t -> Pp.t) -> t -> Pp.t
+
 end
 
 type abstract_universe_context = AUContext.t