coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fast path for set operations.	Pierre-Marie Pédrot	2016-08-22
\| \| \| \| \| \|	We consider an approximation of the size of sets before choosing the most appropriate algorithm. This drastically affects some universe-polymorphic code which was doing a lot of set operations on disimilar sizes.
*	Adding a "get" primitive to map signature.	Pierre-Marie Pédrot	2016-02-03
\| \| \| \| \|	It is similar to find but raises an assertion failure instead of a Not_found when the element is not encountered. Using it will give stronger invariants.
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
\| \|
* \|	Remove some useless module opening.	Guillaume Melquiond	2016-01-02
\| \|
* \|	Equipping extended maps with fold operator defined for any monad.	Pierre-Marie Pédrot	2015-01-25
\|/
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Missing primitives in HMap.	Pierre-Marie Pédrot	2014-07-21
\|
*	Fixing semantics of HSet.inter and HSet.diff.	Pierre-Marie Pédrot	2014-07-21
\|
*	Fixing previous commit. Forgot to include some code.	Pierre-Marie Pédrot	2014-03-05
\|
*	Added a new module HMap. It works (almost) like Map, except that it expects	Pierre-Marie Pédrot	2014-03-05
	the provided type to come with a hashing function. The internal representation is changed, such that values are first compared w.r.t. to their hash. This effectively saves a lot of comparisons which may be far more expensive than O(1), as in the string case, hence resulting in an overall speedup. CAVEAT: everything is not implemented yet, and order-sensitive functions now do not respect the provided order anymore.