aboutsummaryrefslogtreecommitdiff
path: root/clib/hMap.ml
diff options
context:
space:
mode:
Diffstat (limited to 'clib/hMap.ml')
-rw-r--r--clib/hMap.ml4
1 files changed, 4 insertions, 0 deletions
diff --git a/clib/hMap.ml b/clib/hMap.ml
index 3baa105fb0..210c48786b 100644
--- a/clib/hMap.ml
+++ b/clib/hMap.ml
@@ -356,6 +356,10 @@ struct
let (_, m) = Int.Map.choose s in
Map.choose m
+ let choose_opt s =
+ try Some (choose s)
+ with Not_found -> None
+
let find k s =
let h = M.hash k in
let m = Int.Map.find h s in