coq/theories/MMaps/MMapInterface.v, branch master The formal proof system MMaps: remove it from final 8.5 release, since this new library isn't mature enough 2016-01-13T16:38:27+00:00 Pierre Letouzey 2016-01-13T16:38:27+00:00 4b4a4b6b41e6b303d556638ed2a79b1493b1ecf4 In particular, its interface might still change (in interaction with interested colleagues). So let's not give it too much visibility yet. Instead, I'll turn it as an opam packages for now. 
 In particular, its interface might still change (in interaction with interested
 colleagues). So let's not give it too much visibility yet. Instead, I'll turn
 it as an opam packages for now.
Introducing MMaps, a modernized FMaps. 2015-03-04T14:25:21+00:00 Pierre Letouzey 2015-03-04T14:12:46+00:00 00018101cf81f69d23587985a16fe3c8eefb8eaf 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". 
 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".