diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /checker/univ.mli | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Imported Upstream version 8.9.0upstream/8.9.0upstream
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 |