coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Bug 2767	pboutill	2012-05-09
*	Coqide highligthing is back (done by gtksourceview).	pboutill	2012-05-02
*	A notion of permutation for lists modulo a setoid equality	letouzey	2012-05-02
*	remove undocumented and scarcely-used tactic auto decomp	letouzey	2012-04-23
*	Remove the Dp plugin.	gmelquio	2012-04-17
*	Fixing typo in previous commit r15180.	herbelin	2012-04-15
*	Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).	herbelin	2012-04-15
*	MSetRBT : implementation of MSets via Red-Black trees	letouzey	2012-04-13
*	Uniformisation in the documentation: remove the use of 'coinductive' in	aspiwack	2012-04-13
*	"A -> B" is a notation for "forall _ : A, B".	pboutill	2012-04-12
*	Fixing a few bugs (see #2571) related to interpretation of multiple binders	herbelin	2012-04-06
*	Fixing printing level of Utf8 equivalent for ->.	herbelin	2012-03-26
*	Fix interface of resolve_typeclasses: onlyargs -> with_goals:	msozeau	2012-03-20
*	Turning proofs of well-ordering of lexicographic product transparent	herbelin	2012-03-20
*	Fix bugs related to Program integration.	msozeau	2012-03-19
*	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau	2012-03-14
*	Everything compiles again.	msozeau	2012-03-14
*	Remove support for "abstract typing constraints" that requires unicity of sol...	msozeau	2012-03-14
*	Vector: missing injection lemmas and better impossible branches	pboutill	2012-02-29
*	Fix unblocking code in dependent destruction due to zeta being used in unfold...	msozeau	2012-02-01
*	Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...	msozeau	2012-01-31
*	Tentative to fix bug #2628 by not letting intuition break records. Might be t...	msozeau	2012-01-28
*	Fix simplification of ind. hyps., recognized by a [block] in their type (bug ...	msozeau	2012-01-28
*	Deleted the only use of BeginSubProof from the standard library.	ppedrot	2012-01-23
*	No more use of tauto in Init/	pboutill	2012-01-19
*	MSetAVL: better implementation of filter suggested by X. Leroy	letouzey	2012-01-17
*	Added the decidability of (<=) on nat.	ppedrot	2012-01-13
*	Fixed the itarget of the previous commit...	ppedrot	2012-01-06
*	Added a typeclass-based system to reason on decidable propositions.	ppedrot	2012-01-06
*	Granted legitimate wish #2607 (not exposing crude fixpoint body of	herbelin	2011-12-18
*	Vectors use a bit more the pattern matching compiler	pboutill	2011-12-07
*	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge	2011-11-21
*	VectorDef.v takes benefit of dependencies being taken into account	herbelin	2011-11-21
*	Merge subinstances branch by me and Tom Prince.	msozeau	2011-11-17
*	Cleaning a little bit the files talking about descriptions: avoiding	herbelin	2011-11-03
*	Revision 14605 continued (Utf8.v now correctly exporting Utf8_core.v).	herbelin	2011-10-26
*	Merge common notations from Utf8.v and Utf8_core.v (see bug report #2610).	herbelin	2011-10-25
*	Fixing Equality.injectable which did not detect an equality without	herbelin	2011-10-22
*	Fix bug #2586 and enhance clsubst* as well as a side effect	msozeau	2011-10-18
*	Fix bug #2456 and wrong unfolding of lets in the goal due to [unfold] doing z...	msozeau	2011-10-17
*	MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_right	letouzey	2011-10-14
*	Proper fix for complement/flip instances.	msozeau	2011-10-10
*	fsetdec : non-atomic elements are now transformed as variables first (fix #2464)	letouzey	2011-10-07
*	Fix bug #2557 and an issue with Propers for complement	msozeau	2011-10-07
*	Improved handling of element equalities in fsetdec (fix #2467)	letouzey	2011-10-07
*	Removing vernacular code mistakenly committed.	herbelin	2011-10-05
*	Use an ad-hoc monomorphic list in RelationClasses to avoid some universe cons...	letouzey	2011-10-05
*	Moving never-used comments from Zhints.v to dev/doc so as not to	herbelin	2011-10-01
*	Euclid: make the proof transparent (example of extraction in stdlib)	letouzey	2011-09-17
*	Omega: for non-arithmetical goals, try proving False from context (wish #2236)	letouzey	2011-09-16