diff options
| author | Matej Kosik | 2016-08-25 14:31:30 +0200 |
|---|---|---|
| committer | Matej Kosik | 2016-08-25 14:31:30 +0200 |
| commit | a2b0c48d8b531ae1b193eed4dec1afeaa67fbece (patch) | |
| tree | af83d8a0fb79c51e13c44bc60be9cde810f87152 /lib/cMap.mli | |
| parent | 1297523bffdc3a9fe3e447acc6837be835e86d06 (diff) | |
| parent | 7244637f251272c0d0155d49fc7c1af255b7cef8 (diff) | |
Merge remote-tracking branch 'v8.6' into trunk
Diffstat (limited to 'lib/cMap.mli')
| -rw-r--r-- | lib/cMap.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/cMap.mli b/lib/cMap.mli index 3ef7fa2c8a..2838b374ec 100644 --- a/lib/cMap.mli +++ b/lib/cMap.mli @@ -61,6 +61,9 @@ sig val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t (** As [mapi] but tries to preserve sharing. *) + val height : 'a t -> int + (** An indication of the logarithmic size of a map *) + module Unsafe : sig val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t |