summaryrefslogtreecommitdiff
path: root/src/finite_map.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/finite_map.ml')
-rw-r--r--src/finite_map.ml10
1 files changed, 5 insertions, 5 deletions
diff --git a/src/finite_map.ml b/src/finite_map.ml
index fd0a5553..32629fdc 100644
--- a/src/finite_map.ml
+++ b/src/finite_map.ml
@@ -93,11 +93,6 @@ module Fmap_map(Key : Set.OrderedType) : Fmap
let insert m (k,v) = M.add k v m
let union m1 m2 =
M.merge (fun k v1 v2 -> match v2 with | None -> v1 | Some _ -> v2) m1 m2
- let intersect m1 m2 =
- M.fold (fun k v res ->
- if (M.mem k m2)
- then M.add k v res
- else res) M.empty m1
let merge f m1 m2 = M.merge f m1 m2
let apply m k =
try
@@ -117,6 +112,11 @@ module Fmap_map(Key : Set.OrderedType) : Fmap
None
let iter f m = M.iter f m
let fold f m base = M.fold (fun k v res -> f res k v) base m
+ let intersect m1 m2 =
+ M.fold (fun k v res ->
+ if (M.mem k m2)
+ then M.add k v res
+ else res) m1 M.empty
let remove m k = M.remove k m
let pp_map pp_key pp_val ppf m =
let l = M.fold (fun k v l -> (k,v)::l) m [] in