From 016ed06128372e7b767efd4d3e1f71df9ca1e3d4 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 25 Apr 2019 10:32:39 +0200
Subject: Add union in Map interface

---
 kernel/univ.ml  | 17 +++++++----------
 kernel/univ.mli |  4 ++--
 2 files changed, 9 insertions(+), 12 deletions(-)

(limited to 'kernel')

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