coq - The formal proof system

Age	Commit message (Collapse)	Author
2016-08-22	Fast path for set operations.	Pierre-Marie Pédrot
	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.
2016-02-03	Adding a "get" primitive to map signature.	Pierre-Marie Pédrot
	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.
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot

2016-01-20	Update copyright headers.	Maxime Dénès

2016-01-02	Remove some useless module opening.	Guillaume Melquiond

2015-01-25	Equipping extended maps with fold operator defined for any monad.	Pierre-Marie Pédrot

2015-01-12	Update headers.	Maxime Dénès

2014-07-21	Missing primitives in HMap.	Pierre-Marie Pédrot

2014-07-21	Fixing semantics of HSet.inter and HSet.diff.	Pierre-Marie Pédrot

2014-03-05	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
	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.