coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	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
*	Some changes to eliminate Hevea warnings.	emakarov	2007-04-10
*	Split refman/headers.tex into headers.sty and headers.hva.	emakarov	2007-04-10
*	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 du bug #1441	notin	2007-03-16
*	Correction bug #1439 (comportement de replace by)	notin	2007-03-13
*	Application suggestion #1430 de Yevgeniy pour TEXINPUTS	herbelin	2007-03-07
*	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
*	Compilation de la FAQ	notin	2007-02-18
*	Réintroduction de l'entrée "integer" dans ltac (apparemment disparue lors	herbelin	2007-02-15
*	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin	2007-02-13
*	Meilleur anglais (cf 9619)	herbelin	2007-02-07
*	Relecture/nettoyage chapitre Gallina; déplacement section Function	herbelin	2007-02-07
*	Suppression RefMan-cas.tex inutilisé	herbelin	2007-02-07
*	Field rewrites only with polynomial	thery	2007-02-07
*	doc de ring/field + option infinite -> completeness	barras	2007-02-07
*	doc for field	thery	2007-02-06
*	complement du commit 9591	bgregoir	2007-02-05