diff options
Diffstat (limited to 'checker/univ.mli')
| -rw-r--r-- | checker/univ.mli | 12 |
1 files changed, 11 insertions, 1 deletions
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 |