diff options
Diffstat (limited to 'kernel/univ.mli')
| -rw-r--r-- | kernel/univ.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index c06ce2446..f74f29b2c 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -45,6 +45,8 @@ sig val var : int -> t val var_index : t -> int option + + val name : t -> (Names.DirPath.t * int) option end type universe_level = Level.t @@ -121,6 +123,8 @@ sig val exists : (Level.t * int -> bool) -> t -> bool val for_all : (Level.t * int -> bool) -> t -> bool + + val map : (Level.t * int -> 'a) -> t -> 'a list end type universe = Universe.t |