From 328ecf4ea59ab25d891949c35dc9bbec52a5d096 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 29 Aug 2024 16:07:27 -0400 Subject: [PATCH] change API for local FLS hmap --- src/fib/hmap_fls.real.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/fib/hmap_fls.real.ml b/src/fib/hmap_fls.real.ml index 6ed269ac..89ec8701 100644 --- a/src/fib/hmap_fls.real.ml +++ b/src/fib/hmap_fls.real.ml @@ -23,15 +23,15 @@ let[@inline] update_local_hmap (f : Hmap.t -> Hmap.t) : unit = FLS.set fiber k_local_hmap h (** @raise Invalid_argument if not present *) -let get_exn (k : 'a Hmap.key) : 'a = +let get_in_local_hmap_exn (k : 'a Hmap.key) : 'a = let h = get_local_hmap () in Hmap.get k h -let get_opt (k : 'a Hmap.key) : 'a option = +let get_in_local_hmap_opt (k : 'a Hmap.key) : 'a option = let h = get_local_hmap () in Hmap.find k h -let[@inline] set (k : 'a Hmap.key) (v : 'a) : unit = +let[@inline] set_in_local_hmap (k : 'a Hmap.key) (v : 'a) : unit = update_local_hmap (Hmap.add k v) (**/**)