coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Added support for multiple where-clauses in Inductive and co (see wish #2163).	herbelin	2009-11-11
*	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin	2009-11-08
*	Fixed record syntax "{\|x=...; y=...\|}" so that it works with qualified names.	gmelquio	2009-11-04
*	Removed 'Toplevel' language from extraction documentation, since it is not cu...	gmelquio	2009-11-04
*	Report de la révision #12208 de la v8.2 (correction du bug #2126)	notin	2009-11-03
*	Correction du bug #2175	notin	2009-11-02
*	Fixed some typos in the reference manual.	gmelquio	2009-10-29
*	Typo in the refman	puech	2009-10-28
*	Documentation of the Local and Global modifiers.	herbelin	2009-10-27
*	Fix Setoid documentation.	msozeau	2009-10-26
*	New cleaning phase of the Local/Global option management	herbelin	2009-10-26
*	Improved the treatment of Local/Global options (noneffective Local on	herbelin	2009-10-25
*	Fixing XML doc (COQ_XML not working as an environment variable).	herbelin	2009-10-24
*	Repaired bug #2165 (buggy coq example in Tactic Examples doc chapter)	herbelin	2009-10-20
*	typo in doc of Extraction Blacklist	letouzey	2009-10-15
*	Typos.	gmelquio	2009-10-13
*	Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'	letouzey	2009-10-08
*	Fix the stdlib doc compilation + switch all .v file to utf8	letouzey	2009-09-28
*	Micromega doc : psatz Z -> psatz Z 2	fbesson	2009-09-24
*	Ltac doc: only variables are accepted as message_token	glondu	2009-09-23
*	Remove useless MonoList.v	glondu	2009-09-17
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Clarify documentation of ltac repeat	glondu	2009-09-17
*	- Inductive types in the "using" option of auto/eauto/firstorder are	herbelin	2009-09-13
*	Add doc of [Context] vernacular.	msozeau	2009-09-11
*	Removed Gappa from the external provers supported by the dp plugin. Tactic ga...	gmelquio	2009-09-11
*	Added syntax "exists bindings, ..., bindings" for iterated "exists".	herbelin	2009-09-10
*	Update coqdoc documentation, CHANGES and add a fix for the proofbox (patch	msozeau	2009-09-08
*	Fix minor spelling error	glondu	2009-08-29
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 85f007b7-540e-0...	fbesson	2009-08-25
*	Improved parameterization of Coq:	herbelin	2009-08-02
*	Add doc for [Print Opaque Dependencies] and a better explanation for the	msozeau	2009-06-26
*	Report de la révision #12200 (bug #2125)	notin	2009-06-22
*	Applying Ian Lynagh's documentation fixes patch (see bug #2112)	herbelin	2009-06-06
*	- Fixing declarative mode in presence of high use of Change_evars nodes	herbelin	2009-05-20
*	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	herbelin	2009-05-09
*	Backporting 12112 from v8.2 branch to trunk (fixing documentation bugs	herbelin	2009-04-28
*	Document new quote construction	glondu	2009-03-30
*	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey	2009-03-20
*	RefMan: a label defined twice	letouzey	2009-03-14
*	Coqdep: remove references to obsolete .zi and Require Implementation stuff	letouzey	2009-03-14
*	doc et CHANGES pour la commande Timeout	barras	2009-03-04
*	maj de la faq: correction de l'exemple field qui compilait plus en 8.2, corre...	jnarboux	2009-02-17
*	Modification du style du manuel de référence	notin	2009-02-11
*	Solves some warning and hides some not-bad ones in doc. It remains a	herbelin	2009-01-29
*	- Fixed various Overfull in documentation.	herbelin	2009-01-27
*	Fixes in the documentation of [dependent induction] and test-suite	msozeau	2009-01-22
*	Fixed bug 2030 (bad syntax for "test" in doc compilation) [see 11824	herbelin	2009-01-21
*	Added some missing statements for proof folding and corrected	vgross	2009-01-20
*	Added proof folding into CoqIde. See RefMan for using it.	vgross	2009-01-20