From 458cf1324163821b60ab0b731a60bb1977576d9f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 27 Jan 2020 13:29:18 +0100
Subject: 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)
---
 kernel/uGraph.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/uGraph.ml')

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
-- 
cgit v1.2.3