coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Introducing MMaps, a modernized FMaps.	Pierre Letouzey	2015-03-04
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-26
\|\
\| *	Revert "Fixing bug #4035 (support for dependent destruction within ltac code)."	Maxime Dénès	2015-02-26
\| *	Reorder the steps of the easy tactic. (Fix for bug #2630)	Guillaume Melquiond	2015-02-25
* \|	Merge branch 'v8.5' into trunk	Enrico Tassi	2015-02-23
\|\\|
\| *	Fix some typos in comments.	Guillaume Melquiond	2015-02-23
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-18
\|\\|
\| *	Fixing bug #4035 (support for dependent destruction within ltac code).	Hugo Herbelin	2015-02-16
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-15
\|\\|
\| *	dependent destruction: Fix (part of) bug #3961, by fixing dependent *	Matthieu Sozeau	2015-02-14
* \|	Merge branch '8.5' into trunk	Matthieu Sozeau	2015-01-18
\|\\|
* \|	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau	2015-01-18
* \|	Remove typeclass opaque directive, some proofs in the stdlib rely on it being...	Matthieu Sozeau	2015-01-18
* \|	Optionally allow eta-conversion during unification for type classes.	Matthieu Sozeau	2015-01-18
\| *	There was one more universe needed due to the use of now non-universe-polymor...	Matthieu Sozeau	2015-01-18
* \|	Add two lemmas about firstn to the List standard library.	Sébastien Hinderer	2015-01-16
* \|	Lemmas related to the firstn function over lists.	Sébastien Hinderer	2015-01-16
* \|	ListSet: follow-up of Sebastien's last commit	Pierre Letouzey	2015-01-16
* \|	Work in progress on listset.	Sébastien Hinderer	2015-01-16
\| *	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau	2015-01-15
\| *	Remove typeclass opaque directive, some proofs in the stdlib rely on it being...	Matthieu Sozeau	2015-01-15
\| *	Optionally allow eta-conversion during unification for type classes.	Matthieu Sozeau	2015-01-15
\|/
*	Update headers.	Maxime Dénès	2015-01-12
*	Use [Proof using] to make sure that [List.in_flat_map] doesn't grab too many ...	Arnaud Spiwack	2014-12-28
*	Forbid Require inside interactive modules and module types.	Maxime Dénès	2014-12-25
*	Adds two lemmas about hderror to the List standard library.	Sébastien Hinderer	2014-12-18
*	Implement the nodup function on lists and prove associated results.	Sébastien Hinderer	2014-12-18
*	Lists: enhanced version of Seb's last commit on Exists/Forall	Pierre Letouzey	2014-12-18
*	Lists: a few results on Exists and Forall and a bit of code cleanup.	Sébastien Hinderer	2014-12-18
*	Failing on unbound notation variable in notation level modifiers	Hugo Herbelin	2014-12-15
*	List.v: sequel to Sebastien's commit (some cosmetics + a few shorter proofs)	Pierre Letouzey	2014-12-11
*	First series of results on lists.	Sébastien Hinderer	2014-12-11
*	Added an arithmetical characterization of the hypothesis of WKL.	Hugo Herbelin	2014-12-01
*	Clarifying the role of ListSet.v in the library, compared to other	Hugo Herbelin	2014-11-18
*	Enforcing a stronger difference between the two syntaxes "simpl	Hugo Herbelin	2014-11-16
*	Improving elimination with indices, getting rid of intrusive residual	Hugo Herbelin	2014-11-02
*	Supporting "at occs" as a short-hand for "in \|- * at occs" in "destruct".	Hugo Herbelin	2014-11-02
*	Make sure that Logic/ExtensionalityFacts gets compiled.	Guillaume Melquiond	2014-10-27
*	Fix some typos.	Guillaume Melquiond	2014-10-27
*	Fix some typos in comments.	Guillaume Melquiond	2014-10-27
*	EqdepFacts: generalize statements which were wrongly restricted to Prop.	Arnaud Spiwack	2014-10-22
*	Fixing typo absorption (bug #3751).	Hugo Herbelin	2014-10-22
*	Revert "Essai où assert_style n'est utilisé que si pas visuellement une éq...	Hugo Herbelin	2014-10-17
*	Essai où assert_style n'est utilisé que si pas visuellement une équation;	Hugo Herbelin	2014-10-17
*	ConstructiveEpsilon: simplify the before_witness type using non-uniform param...	Arnaud Spiwack	2014-10-16
*	Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name	Matthieu Sozeau	2014-10-11
*	Give the same argument name for the record binder of type class	Matthieu Sozeau	2014-10-10
*	Fix segfault in native compiler on int31 division.	Maxime Dénès	2014-10-10
*	eta contractions	Pierre Boutillier	2014-10-01
*	argument flip of Cyclic31.nshiftr and Cyclic31.nshiftl	Pierre Boutillier	2014-10-01