aboutsummaryrefslogtreecommitdiff
path: root/clib/hMap.ml
diff options
context:
space:
mode:
Diffstat (limited to 'clib/hMap.ml')
-rw-r--r--clib/hMap.ml6
1 files changed, 6 insertions, 0 deletions
diff --git a/clib/hMap.ml b/clib/hMap.ml
index 9c80398e4d..5d634b7af0 100644
--- a/clib/hMap.ml
+++ b/clib/hMap.ml
@@ -353,6 +353,12 @@ struct
let m = Int.Map.find h s in
Map.find k m
+ let find_opt k s =
+ let h = M.hash k in
+ match Int.Map.find_opt h s with
+ | None -> None
+ | Some m -> Map.find_opt k m
+
let get k s = try find k s with Not_found -> assert false
let split k s = assert false (** Cannot be implemented efficiently *)