Add union in Map interface

6 files changed, 21 insertions, 14 deletions

diff --git a/clib/cSig.mli b/clib/cSig.mli
index 859018ca4b..0012bcef17 100644
--- a/clib/cSig.mli
+++ b/clib/cSig.mli
@@ -68,6 +68,8 @@ sig
     val remove: key -> 'a t -> 'a t
     val merge:
          (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
+    val union:
+      (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
     val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
     val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
     val iter: (key -> 'a -> unit) -> 'a t -> unit
diff --git a/clib/hMap.ml b/clib/hMap.ml
index 09ffb39c21..db59ef47b0 100644
--- a/clib/hMap.ml
+++ b/clib/hMap.ml
@@ -290,6 +290,14 @@ struct
     in
     Int.Map.merge fm s1 s2
 
+  let union f s1 s2 =
+    let fm h m1 m2 =
+      let m = Map.union f m1 m2 in
+      if Map.is_empty m then None
+      else Some m
+    in
+    Int.Map.union fm s1 s2
+
   let compare f s1 s2 =
     let fc m1 m2 = Map.compare f m1 m2 in
     Int.Map.compare fc s1 s2
diff --git a/engine/uState.ml b/engine/uState.ml
index 6f4f40e2c5..aa14f66df6 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -85,7 +85,7 @@ let union ctx ctx' =
     let declarenew g =
       LSet.fold (fun u g -> UGraph.add_universe u false g) newus g
     in
-    let names_rev = LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in
+    let names_rev = LMap.lunion (snd ctx.uctx_names) (snd ctx'.uctx_names) in
       { uctx_names = (names, names_rev);
         uctx_local = local;
         uctx_seff_univs = seff;
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index 46ff6340b4..fcbf305f9d 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -203,7 +203,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
           (acc, [], LMap.empty, LMap.empty) l
         in
         let left = CList.uniquize (List.filter (not_lower lower) left) in
-        (acc, left, LMap.union newlow lower)
+        (acc, left, LMap.lunion newlow lower)
     in
     let instantiate_lbound lbound =
       let alg = LSet.mem u algs in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 8263c68bf5..b1bbc25fe6 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -231,18 +231,15 @@ module LMap = struct
   module M = HMap.Make (Level)
   include M
 
-  let union l r = 
-    merge (fun _k l r ->
-      match l, r with
-      | Some _, _ -> l
-      | _, _ -> r) l r
+  let lunion l r =
+    union (fun _k l _r -> Some l) l r
 
-  let subst_union l r = 
-    merge (fun _k l r ->
+  let subst_union l r =
+    union (fun _k l r ->
       match l, r with
-      | Some (Some _), _ -> l
-      | Some None, None -> l
-      | _, _ -> r) l r
+      | Some _, _ -> Some l
+      | None, None -> Some l
+      | _, _ -> Some r) l r
 
   let diff ext orig =
     fold (fun u v acc -> 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 5543c35741..db178c4bb0 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -223,8 +223,8 @@ module LMap :
 sig
   include CMap.ExtS with type key = Level.t and module Set := LSet
 
-  val union : 'a t -> 'a t -> 'a t
-  (** [union x y] favors the bindings in the first map. *)
+  val lunion : 'a t -> 'a t -> 'a t
+  (** [lunion x y] favors the bindings in the first map. *)
 
   val diff : 'a t -> 'a t -> 'a t
   (** [diff x y] removes bindings from x that appear in y (whatever the value). *)