coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- Documentation des nouvelles options d'implicites (Set Strongly Strict	herbelin	2008-02-06
*	Add new files theories/Program/Basics.v and theories/Classes/Relations.v	msozeau	2008-02-03
*	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
*	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
*	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
*	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
*	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
*	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
*	Documentation of Program and its tactics, fix enormous interaction bug due to...	msozeau	2007-07-19
*	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
*	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
*	Changed many refman/*.tex files. Put \label and \index commands that immediat...	emakarov	2007-04-17
*	Removed from headers.hva the code to make index point to the section	emakarov	2007-04-16
*	Cleaned doc/common/title.tex file. Increased the space under headers	emakarov	2007-04-12
*	Standardisation format biblio	herbelin	2007-04-12
*	Eliminated warning messages from Hevea. Most warning messages were	emakarov	2007-04-10
*	Mise en place d'un rafinement de compute.	jforest	2007-04-05
*	Corrected a typo in doc/refman/Setoid.tex.	emakarov	2007-04-04
*	Correction bug #1439 (comportement de replace by)	notin	2007-03-13
*	doc: typo/english: "is left associating" -> "is left-associative".	lmamane	2007-02-22
*	Documentation of tactical "t1 \|\| t2": t2 is executed if t1 fails to	lmamane	2007-02-22