diff options
| author | Gaëtan Gilbert | 2018-12-15 12:11:56 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-12-17 14:48:45 +0100 |
| commit | 5421b17f22b09ecca688a989a268385005dad01b (patch) | |
| tree | 86322374b01ca3663e07a87569b730ad51756384 /clib/cSig.mli | |
| parent | 854d3e1b404fb3ee9087ffb07cbba7cc9196c1f9 (diff) | |
Add Map.find_opt
Diffstat (limited to 'clib/cSig.mli')
| -rw-r--r-- | clib/cSig.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/clib/cSig.mli b/clib/cSig.mli index fb36cc5b51..859018ca4b 100644 --- a/clib/cSig.mli +++ b/clib/cSig.mli @@ -83,6 +83,7 @@ sig val choose: 'a t -> (key * 'a) val split: key -> 'a t -> 'a t * 'a option * 'a t val find: key -> 'a t -> 'a + val find_opt : key -> 'a t -> 'a option val map: ('a -> 'b) -> 'a t -> 'b t val mapi: (key -> 'a -> 'b) -> 'a t -> 'b t end |