diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-07-21 19:07:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-07-21 19:07:48 +0200 |
| commit | c4ecec191130a51975bf97d067472e0e5bd744f5 (patch) | |
| tree | d470e28a2495ec90321260543550f5f62418b1dd /lib/hMap.ml | |
| parent | e9be775a92869a371d229c9bfebcd0c7270122b7 (diff) | |
Fixing semantics of HSet.inter and HSet.diff.
Diffstat (limited to 'lib/hMap.ml')
| -rw-r--r-- | lib/hMap.ml | 5 |
1 files changed, 3 insertions, 2 deletions
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 |