aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorGuillaume Melquiond2016-01-02 17:01:28 +0100
committerGuillaume Melquiond2016-01-02 17:01:28 +0100
commit3049b2930ec2bd4adf886fc90bf01a478b318477 (patch)
tree00ff808e57abcbc2dcb1775707d26dd9eeba3692 /lib
parent57c7d751df85366ba3781c4e1107a745a660714d (diff)
Remove some useless module opening.
Diffstat (limited to 'lib')
-rw-r--r--lib/hMap.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/lib/hMap.ml b/lib/hMap.ml
index 8e900cd581..b5fc523150 100644
--- a/lib/hMap.ml
+++ b/lib/hMap.ml
@@ -333,7 +333,6 @@ struct
struct
module IntM = Int.Map.Monad(M)
module ExtM = Map.Monad(M)
- open M
let fold f s accu =
let ff _ m accu = ExtM.fold f m accu in