New functions introduced:
Incr_map.merge_disjoint merges two maps with disjoint keysIncr_map.observe_changes_exn observes changes in a map across stabilizationsIncr_map
New functions
cutoff - applies a cutoff to the values in an incremental mappartition_mapi' - like partition_mapi, but the callback function has an incremental input and outputunordered_fold_with_extra - like unordered_fold, but depends on an arbitrary extra incremental value that can be factored into the folding computationmerge_both_some - like merge, but the mapping callback function is only called on keys contained in both mapsNew arguments
Instrumentation module and optional instrumentation argument to all Incr_map functions, which can be used for performance profilingfinalize argument to unordered_fold, which can be used to change the order in which fold operations are processedBug fixes
subrange_by_rank to handle unbounded lower bound correctlymapi_mn to map_minErase_key
Collate
Remove the Map_list library
Map_list to the more general Incr_map_erase_keyIncr_map_collate no longer a functorFold
Fold defining a fold callback functioncollate_and_fold, like collate but allows you to perform a fold over the post-filtered, pre-range-restricted datacollate_and_fold__sort_first, like collate__sort_first but allows you to perform a fold over the post-filtered, pre-range-restricted data