From 0545a39afffcb7e711245c69d41f6b266004aa44 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 30 Aug 2024 09:46:49 -0400 Subject: [PATCH] add Task_local_storage.remove_in_local_hmap --- src/core/hmap_ls_.real.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/core/hmap_ls_.real.ml b/src/core/hmap_ls_.real.ml index ef4e078f..b9c0194d 100644 --- a/src/core/hmap_ls_.real.ml +++ b/src/core/hmap_ls_.real.ml @@ -31,6 +31,10 @@ let get_in_local_hmap_opt (k : 'a Hmap.key) : 'a option = let h = get_local_hmap () in Hmap.find k h +(** Remove given key from the local hmap *) +let[@inline] remove_in_local_hmap (k : _ Hmap.key) : unit = + update_local_hmap (Hmap.rem k) + let[@inline] set_in_local_hmap (k : 'a Hmap.key) (v : 'a) : unit = update_local_hmap (Hmap.add k v)