From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 checker/univ.mli | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'checker/univ.mli')

diff --git a/checker/univ.mli b/checker/univ.mli
index 473159c0..3b29b158 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
@@ -138,7 +139,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} *)
@@ -214,6 +222,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
-- 
cgit v1.2.3