aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2015-03-04 15:12:46 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2015-03-04 15:25:21 +0100
commit00018101cf81f69d23587985a16fe3c8eefb8eaf (patch)
tree4d64d51f18403975aec5d396c88664fdb8004343 /toplevel
parent85fc5f90c52a755d1b64640f4f0b3421979c0fe8 (diff)
Introducing MMaps, a modernized FMaps.
NB: this is work-in-progress, there is currently only one provided implementation (MMapWeakList). In the same spirit as MSets w.r.t FSets, the main difference between MMaps and former FMaps is the use of a new version of OrderedType (see Orders.v instead of obsolete OrderedType.v). We also try to benefit more from recent notions such as Proper. For most function specifications, the style has changed : we now use equations over "find" instead of "MapsTo" predicates, whenever possible (cf. Maps in Compcert for a source of inspiration). Former specs are now derived in FMapFacts, so this is mostly a matter of taste. Two changes inspired by the current Maps of OCaml: - "elements" is now "bindings" - "map2" is now "merge" (and its function argument also receives a key). We now use a maximal implicit argument for "empty".
Diffstat (limited to 'toplevel')
0 files changed, 0 insertions, 0 deletions