coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Extension of the recursive notations mechanism	herbelin	2010-07-22
*	FSetPositive: sets of positive inspired by FMapPositive.	letouzey	2010-07-16
*	Updating reference manual credits: gb is now nsatz.	herbelin	2010-07-08
*	Update of documentation for the standard library (cf. #2332)	letouzey	2010-06-28
*	Applying François' patches about Canonical Projections (see #2302 and #2334).	herbelin	2010-06-26
*	modifs de nsatz suggerees par Hugo	pottier	2010-06-25
*	Ajout d'une feuille de style pour les définitions spécifiques à Hevea + di...	notin	2010-06-23
*	Mise à jour des liens au site Coq (suite à la MAJ de la redirection DNS de ...	notin	2010-06-23
*	Documentation of clear dependent and revert dependent	letouzey	2010-06-18
*	Update of Extraction documentation	letouzey	2010-06-14
*	Extraction Implicit: documentation	letouzey	2010-06-14
*	Reverted commit 13110 about headers.sty that I wrongly thought was buggy. Sorry.	herbelin	2010-06-11
*	Fixed a very old (from V6.3) typo in headers.sty	herbelin	2010-06-10
*	Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".	herbelin	2010-06-08
*	Backporting part of r12970 to trunk (deprecation of double induction).	herbelin	2010-06-07
*	doc Nstaz updated	pottier	2010-06-04
*	A new command Compute foo, shortcut for Eval vm_compute in foo	letouzey	2010-06-04
*	ajout oublie	pottier	2010-06-03
*	plugin groebner updated and renamed as nsatz; first version of the doc of nsa...	pottier	2010-06-03
*	Minor fix in doc chapter on inference rules (added a missing space).	herbelin	2010-05-28
*	Extract Inductive is now possible toward non-inductive types (e.g. nat => int)	letouzey	2010-05-21
*	Remove compile-command pragmas for emacs	letouzey	2010-05-19
*	Some ocamldoc comments + Fixing name of .coqrc.version file in refman	pboutill	2010-05-18
*	Update of credits files	herbelin	2010-05-09
*	Correction in Function documentation	jforest	2010-05-06
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	small detail about Scheme Equality	vsiles	2010-04-27
*	Applying François Garillot's patch (#2261 in bug tracker) for extended	herbelin	2010-04-22
*	Documenting the use of ##, %%, $$ in coqdoc.	herbelin	2010-04-09
*	Applied Cédric Auger's patch to fix use of "#&xxx;" in html printing	herbelin	2010-04-09
*	Add documentation on the treatment of [if] and [let (x1, ... xn) := ..]	msozeau	2010-03-31
*	Update manual on search commands	puech	2010-03-11
*	Correction du bug #2214 + maj liens web	notin	2010-02-26
*	Polishing the setup of CoqIDE Input Method	vgross	2010-02-18
*	Documentation of the ! annotation for functor application	letouzey	2010-02-11
*	Fix [Existing Class] impl and add documentation. Fix computation of the	msozeau	2010-02-10
*	Update CHANGES, add documentation for new commands/tactics and do a bit	msozeau	2010-01-30
*	New command Declare Reduction <id> := <conv_expr>.	letouzey	2010-01-28
*	Document Local Declare ML Module	glondu	2010-01-14
*	Include can accept both Module and Module Type	letouzey	2010-01-07
*	Specific syntax for Instances in Module Type: Declare Instance	letouzey	2010-01-04
*	Patches and instructions to enable Input Method support in CoqIDE.	vgross	2009-12-21
*	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-12-15
*	Document Generalizable Variables, and change syntax to	msozeau	2009-11-15
*	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