diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/univ.ml | 22 | ||||
| -rw-r--r-- | kernel/univ.mli | 4 |
2 files changed, 16 insertions, 10 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 64afb95d56..8cf9028fb1 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -192,6 +192,10 @@ module Level = struct let make m n = make (Level (n, Names.DirPath.hcons m)) + let name u = + match data u with + | Level (n, d) -> Some (d, n) + | _ -> None end (** Level maps *) @@ -337,19 +341,16 @@ struct returning [SuperSame] if they refer to the same level at potentially different increments or [SuperDiff] if they are different. The booleans indicate if the left expression is "smaller" than the right one in both cases. *) - let super (u,n as x) (v,n' as y) = + let super (u,n) (v,n') = let cmp = Level.compare u v in if Int.equal cmp 0 then SuperSame (n < n') else - match x, y with - | (l,0), (l',0) -> - let open RawLevel in - (match Level.data l, Level.data l' with - | Prop, Prop -> SuperSame false - | Prop, _ -> SuperSame true - | _, Prop -> SuperSame false - | _, _ -> SuperDiff cmp) - | _, _ -> SuperDiff cmp + let open RawLevel in + match Level.data u, n, Level.data v, n' with + | Prop, _, Prop, _ -> SuperSame (n < n') + | Prop, 0, _, _ -> SuperSame true + | _, _, Prop, 0 -> SuperSame false + | _, _, _, _ -> SuperDiff cmp let to_string (v, n) = if Int.equal n 0 then Level.to_string v @@ -499,6 +500,7 @@ struct let smartmap = List.smartmap + let map = List.map end type universe = Universe.t diff --git a/kernel/univ.mli b/kernel/univ.mli index c06ce2446f..f74f29b2c1 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 |