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
\| \|
* \|	Merge remote-tracking branch 'origin/v8.5' into trunk	Guillaume Melquiond	2016-01-06
\|\\| \| \| \| \| \| \| \| \|	Conflicts: lib/cSig.mli
\| *	Protect code against changes in Map interface.	Maxime Dénès	2016-01-06
\| \| \| \| \| \| \| \| \| \| \| \|	The Map interface of upcoming OCaml 4.03 includes a new union operator. In order to make our homemade implementation of Maps compatible with OCaml versions from 3.12 to 4.03, we define our own signatures for Maps.
* \|	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
\|
*	"allows to", like "allowing to", is improper	Jason Gross	2014-08-25
\| \| \| \| \| \| \| \| \| \| \|	It's possible that I should have removed more "allows", as many instances of "foo allows to bar" could have been replaced by "foo bars" (e.g., "[Qed] allows to check and save a complete proof term" could be "[Qed] checks and saves a complete proof term"), but not always (e.g., "the optional argument allows to ignore universe polymorphism" should not be "the optional argument ignores universe polymorphism" but "the optional argument allows the caller to instruct Coq to ignore universe polymorphism" or something similar).
*	Fixing compilation on OCaml 4.01.	Pierre-Marie Pédrot	2014-03-05
\|
*	Adding a smartmap[i] operator to maps.	Pierre-Marie Pédrot	2014-01-29
\|
*	Adding fold_left / fold_right function to maps.	Pierre-Marie Pédrot	2013-11-24
\|
*	Adding an unsafe mapping function to maps.	ppedrot	2013-11-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17085 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added an update function in CMap. It has the same signature as Map.add, but	ppedrot	2013-11-04
\| \| \| \| \| \|	expects the given key to be present, and thus is faster. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17051 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a [modify] function to maps.	ppedrot	2013-10-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16853 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removing association lists in Reductionops. Btw, defining the dual of the	ppedrot	2013-08-25
\| \| \| \| \| \|	domain operation on maps. The efficiency should just be improved. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16737 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a more efficient way to recover the domain of a map.	ppedrot	2013-08-25
	The extended signature is defined in CMap, and should be compatible with the old one, except that module arguments have to be explicitely named. The implementation itself is quite unsafe, as it relies on the current implementation of OCaml maps, even though that should not be a problem (it has not changed in ages). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16735 85f007b7-540e-0410-9357-904b9bb8a0f7