Small API additions to kernel/univ

- allow viewing the internal representation of uglobal and universe
  (with universe, this replaces the "map" function. I kept exists and
  for_all as they felt somewhat convenient)
- add universe set and map modules (currently unused but they're natural)

1 files changed, 1 insertions, 1 deletions

diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 33336079bb..4d15ce741c 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -128,7 +128,7 @@ let enforce_leq_alg u v g =
          | exception (UniverseInconsistency _ as e) -> Inr e)
   in
   (* max(us) <= max(vs) <-> forall u in us, exists v in vs, u <= v *)
-  let c = Universe.map (fun u -> Universe.map (fun v -> (u,v)) v) u in
+  let c = List.map (fun u -> List.map (fun v -> (u,v)) (Universe.repr v)) (Universe.repr u) in
   let c = List.cartesians enforce_one (Inl (Constraint.empty,g)) c in
   (* We pick a best constraint: smallest number of constraints, not an error if possible. *)
   let order x y = match x, y with