coq - The formal proof system

Age	Commit message (Collapse)	Author
2016-01-13	MMaps: remove it from final 8.5 release, since this new library isn't mature ↵	Pierre Letouzey
	enough 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.
2015-12-07	Fix some typos.	Guillaume Melquiond

2015-04-02	MMapAVL: some improved proofs + fix a forgotten Admitted	Pierre Letouzey

2015-04-02	MMapAVL: implementing MMapInterface via AVL trees	Pierre Letouzey

2015-04-02	MMapPositive: some improvements	Pierre Letouzey
	Most of them are backports of improvements already there in FSetPositive when compared with the original FMapPositive file.
2015-03-06	MMapPositive: another implementation of MMaps	Pierre Letouzey

2015-03-05	MMaps again : adding MMapList, an implementation by ordered list	Pierre Letouzey

2015-03-04	Introducing MMaps, a modernized FMaps.	Pierre Letouzey
	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".