diff options
| author | Maxime Dénès | 2019-04-25 10:32:39 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-02 12:28:19 +0200 |
| commit | 016ed06128372e7b767efd4d3e1f71df9ca1e3d4 (patch) | |
| tree | 84a2c5c5a68ab9fefce2436e137cd608861b1c70 /kernel | |
| parent | ef0ef9f318a0af6542835b71ce7aaced021fff6d (diff) | |
Add union in Map interface
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/univ.ml | 17 | ||||
| -rw-r--r-- | kernel/univ.mli | 4 |
2 files changed, 9 insertions, 12 deletions
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). *) |