coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fix some typos.	Guillaume Melquiond	2015-12-07
\|
*	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	2015-04-02
\| \| \| \| \|	Most of them are backports of improvements already there in FSetPositive when compared with the original FMapPositive file.
*	MMapPositive: another implementation of MMaps	Pierre Letouzey	2015-03-06
\|
*	MMaps again : adding MMapList, an implementation by ordered list	Pierre Letouzey	2015-03-05
\|
*	Introducing MMaps, a modernized FMaps.	Pierre Letouzey	2015-03-04
	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".