coq - The formal proof system

Age	Commit message (Expand)	Author
2009-09-24	Micromega doc : psatz Z -> psatz Z 2	fbesson
2009-09-23	Ltac doc: only variables are accepted as message_token	glondu
2009-09-17	Clarify documentation of ltac repeat	glondu
2009-09-13	- Inductive types in the "using" option of auto/eauto/firstorder are	herbelin
2009-09-11	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-10	Added syntax "exists bindings, ..., bindings" for iterated "exists".	herbelin
2009-09-08	Update coqdoc documentation, CHANGES and add a fix for the proofbox (patch	msozeau
2009-08-29	Fix minor spelling error	glondu
2009-08-25	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 85f007b7-540e-0...	fbesson
2009-08-02	Improved parameterization of Coq:	herbelin
2009-06-26	Add doc for [Print Opaque Dependencies] and a better explanation for the	msozeau
2009-06-22	Report de la révision #12200 (bug #2125)	notin
2009-06-06	Applying Ian Lynagh's documentation fixes patch (see bug #2112)	herbelin
2009-05-20	- Fixing declarative mode in presence of high use of Change_evars nodes	herbelin
2009-05-09	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	herbelin
2009-04-28	Backporting 12112 from v8.2 branch to trunk (fixing documentation bugs	herbelin
2009-03-30	Document new quote construction	glondu
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey
2009-03-14	RefMan: a label defined twice	letouzey
2009-03-14	Coqdep: remove references to obsolete .zi and Require Implementation stuff	letouzey
2009-03-04	doc et CHANGES pour la commande Timeout	barras
2009-02-11	Modification du style du manuel de référence	notin
2009-01-27	- Fixed various Overfull in documentation.	herbelin
2009-01-22	Fixes in the documentation of [dependent induction] and test-suite	msozeau
2009-01-20	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-19	- Structuring Numbers and fixing Setoid in stdlib's doc.	herbelin
2009-01-18	Backporting from v8.2 to trunk:	herbelin
2009-01-18	Last changes in type class syntax:	msozeau
2009-01-13	Updated dates	herbelin
2009-01-13	- Standardized prefix use of "Local"/"Global" modifiers as decided in	herbelin
2009-01-08	Minor doc fixes:	msozeau
2009-01-03	Fixed two problems:	herbelin
2009-01-01	- Fixed bug #2021 (uncaught exception with injection/discriminate when	herbelin
2008-12-29	- Added support for subterm matching in SearchAbout.	herbelin
2008-12-24	- coq_makefile: target install now respects the original tree structure	herbelin
2008-12-16	Extraction Blacklist : a new command for avoiding conflicts with existing files	letouzey
2008-12-14	Fixes in the type classes documentation:	msozeau
2008-12-09	About "apply in":	herbelin
2008-11-28	Inductive parameters: nicer doc examples and error message	letouzey
2008-11-22	- Fixed minor bug #1994 in the tactic chapter of the manual [doc]	herbelin
2008-11-19	Fix typo in omega doc	glondu
2008-10-29	Document native "Declare ML Module"	glondu
2008-10-27	- Fixed many "Theorem with" bugs.	herbelin
2008-10-24	Fix doc of apply in (see coq-club message 26 September 2008)	herbelin
2008-10-20	Renommage "Global Instance" en "Instance Global" pour uniformisation	herbelin
2008-10-19	- Export de pattern_ident vers les ARGUMENT EXTEND and co.	herbelin
2008-10-14	report de la révision r11451 (nouveau style html pour le manuel de référence)	notin
2008-10-11	Backporting 11445 from 8.2 to trunk (negative conditions in	herbelin