From c4ecec191130a51975bf97d067472e0e5bd744f5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 21 Jul 2014 19:07:40 +0200 Subject: Fixing semantics of HSet.inter and HSet.diff. --- lib/hMap.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'lib/hMap.ml') diff --git a/lib/hMap.ml b/lib/hMap.ml index 73cfbd0c7..ea70e152d 100644 --- a/lib/hMap.ml +++ b/lib/hMap.ml @@ -79,7 +79,7 @@ struct let inter s1 s2 = let fu _ m1 m2 = match m1, m2 with | None, None -> None - | (Some _ as m), None | None, (Some _ as m) -> m + | (Some _ as m), None | None, (Some _ as m) -> None | Some m1, Some m2 -> let m = Set.inter m1 m2 in if Set.is_empty m then None else Some m @@ -89,7 +89,8 @@ struct let diff s1 s2 = let fu _ m1 m2 = match m1, m2 with | None, None -> None - | (Some _ as m), None | None, (Some _ as m) -> m + | (Some _ as m), None -> m + | None, (Some _ as m) -> None | Some m1, Some m2 -> let m = Set.diff m1 m2 in if Set.is_empty m then None else Some m -- cgit v1.2.3