coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Unification de TacLetRecIn et TacLetIn. En particulier, on peut	herbelin	2008-02-01
*	Debug implementation of dependent induction/dependent destruction and documen...	msozeau	2008-01-31
*	Finish let\| implementation and document it	msozeau	2008-01-31
*	Added full documentation for mathematical mode (draft version)	corbinea	2008-01-29
*	Ajout d'une explication dans la FAQ pour le bug avec MOD4 sous Coqide	notin	2008-01-07
*	Added a note about the ambiguity of the syntax "qualid" in "tacarg"	herbelin	2008-01-05
*	Standardisation du format des références croisées vers Figure, Section, Ch...	herbelin	2008-01-05
*	Maj du lien vers coq-bugs dans Coqide.	glondu	2007-12-18
*	Modification de la question no 172 de la FAQ (cf bug #1755)	notin	2007-12-11
*	Ajout de l'axiomatisation des entiers à la documentation de la librairie sta...	notin	2007-11-28
*	Doc update	msozeau	2007-10-24
*	Added the doc for the new Scheme Equality command	vsiles	2007-10-16
*	documentation of commit 10188	letouzey	2007-10-08
*	Révision de theories/Logic concernant les axiomes de descriptions.	herbelin	2007-10-03
*	Fix a problem doing 'make clean' under Winodws	notin	2007-10-02
*	Changes in Backtrack documentation. More accurate.	courtieu	2007-09-25
*	Added the documentation for Backtrack and BackTo.	courtieu	2007-09-24
*	Indication de quel type de constantes est dépliable dans "simpl" (cf	herbelin	2007-09-19
*	MAJ date copyright doc	herbelin	2007-09-18
*	A word on the measure and wf modifiers	msozeau	2007-09-01
*	Mise à jour des paramètres Whelp et ajouts d'options Set Whelp Server	herbelin	2007-08-30
*	Add info on measure based defs.	msozeau	2007-08-26
*	Save IS NOT the same Defined ....	msozeau	2007-08-22
*	Erreur de copier/coller dans la section Guarded	notin	2007-08-20
*	Correction du bug #1635	notin	2007-08-13
*	Modification de control_only_guard, qui utilise maintenant	notin	2007-08-09
*	A better Program documentation. Include it in the generated stdlib doc.	msozeau	2007-08-08
*	Move Program tactics into a proper theories/ directory as they are general pu...	msozeau	2007-08-07
*	Corrected the reference to glob.dump, which is used to create stdlib/index-bo...	emakarov	2007-07-26
*	Modifications de la construction de la documentation de la librairie	notin	2007-07-25
*	Documentation of Program and its tactics, fix enormous interaction bug due to...	msozeau	2007-07-19
*	New bootstrapping, improved, Makefile system	corbinea	2007-07-13
*	port de r9968: bug avec les ring calculatoires	barras	2007-07-12
*	More natural notation for intro pattern: @a -> ?a	glondu	2007-07-09
*	If a fixpoint is not written with an explicit { struct ... }, then	letouzey	2007-07-07
*	Adding a syntax for "n-ary" rewrite:	letouzey	2007-07-06
*	extension of the rename tactic: the following is now allowed:	letouzey	2007-07-06
*	New intro pattern "@A", which generates a fresh name based on A.	glondu	2007-07-06
*	Documentation related to commit 9948: intropattern {A,B,C} for (A,(B,C))	letouzey	2007-07-06
*	documentation of f_equal and revert and case_eq (and s/lri.fr/pps.jussieu.fr/...	letouzey	2007-07-05
*	typo faq	herbelin	2007-06-19
*	Removed an extra \tacindex occurrence for the tactic discriminate.	emakarov	2007-06-08
*	Ajout doc clear sans argument	herbelin	2007-06-07
*	Fixed bug #1540 (typo on name .coqide-gtk2rc)	herbelin	2007-05-17
*	- MAJ entêtes des fichiers produits par coq_makefile	herbelin	2007-05-16
*	Made some places in the reference manual clearer. Corrected	emakarov	2007-05-11
*	Ajout possibilité d'options à trois mots.	herbelin	2007-04-29
*	Documentation de Existential et de Show Existential (fixes bug #1294)	notin	2007-04-26
*	Fixed some typos.	glondu	2007-04-18
*	Corrected a LaTeX typo.	emakarov	2007-04-17