coq - The formal proof system

Age	Commit message (Expand)	Author
2010-03-11	Update manual on search commands	puech
2010-02-26	Correction du bug #2214 + maj liens web	notin
2010-02-18	Polishing the setup of CoqIDE Input Method	vgross
2010-02-11	Documentation of the ! annotation for functor application	letouzey
2010-02-10	Fix [Existing Class] impl and add documentation. Fix computation of the	msozeau
2010-01-30	Update CHANGES, add documentation for new commands/tactics and do a bit	msozeau
2010-01-28	New command Declare Reduction <id> := <conv_expr>.	letouzey
2010-01-14	Document Local Declare ML Module	glondu
2010-01-07	Include can accept both Module and Module Type	letouzey
2010-01-04	Specific syntax for Instances in Module Type: Declare Instance	letouzey
2009-12-21	Patches and instructions to enable Input Method support in CoqIDE.	vgross
2009-12-15	Description of the new features of the module system (part two).	soubiran
2009-12-15	Description of the new features of the module system (first part).	soubiran
2009-11-15	Document Generalizable Variables, and change syntax to	msozeau
2009-11-11	Added support for multiple where-clauses in Inductive and co (see wish #2163).	herbelin
2009-11-08	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin
2009-11-04	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-03	Report de la révision #12208 de la v8.2 (correction du bug #2126)	notin
2009-11-02	Correction du bug #2175	notin
2009-10-29	Fixed some typos in the reference manual.	gmelquio
2009-10-28	Typo in the refman	puech
2009-10-27	Documentation of the Local and Global modifiers.	herbelin
2009-10-26	Fix Setoid documentation.	msozeau
2009-10-26	New cleaning phase of the Local/Global option management	herbelin
2009-10-25	Improved the treatment of Local/Global options (noneffective Local on	herbelin
2009-10-24	Fixing XML doc (COQ_XML not working as an environment variable).	herbelin
2009-10-20	Repaired bug #2165 (buggy coq example in Tactic Examples doc chapter)	herbelin
2009-10-15	typo in doc of Extraction Blacklist	letouzey
2009-10-13	Typos.	gmelquio
2009-10-08	Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'	letouzey
2009-09-28	Fix the stdlib doc compilation + switch all .v file to utf8	letouzey
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	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-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