coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Ajout infos de débogage de "universe inconsistency" quand option Set	herbelin	2007-09-30
*	Creation of a new token PATTERNIDENT (?ident) for intro patterns, so	glondu	2007-09-28
*	On empêche "fresh" d'engendrer un mot-clé.	herbelin	2007-09-28
*	On Linux, we read /proc/self/exe to get the executable's path instead	glondu	2007-09-28
*	Correction bug 1711	herbelin	2007-09-28
*	Oubli dans Setoid.v	notin	2007-09-28
*	Forget to update the CHANGES file	vsiles	2007-09-28
*	Modification of the Scheme command.	vsiles	2007-09-28
*	Découpage de Setoid.v	notin	2007-09-27
*	Reals: prod_f_SO inclut f(0) dans le produit et devient prod_f_R0	herbelin	2007-09-27
*	Complément aux commits 10124 et 10125 sur l'inférence de type (correction	herbelin	2007-09-26
*	added a lemma to prove inj_pair2 when eq_dec is available.	vsiles	2007-09-26
*	An update on theories/Numbers.	emakarov	2007-09-25
*	Changes in Backtrack documentation. More accurate.	courtieu	2007-09-25
*	Suppression de tous les alias de la forme x:=x dans la compilation du filtrage.	herbelin	2007-09-25
*	Added the documentation for Backtrack and BackTo.	courtieu	2007-09-24
*	curpat_ty was in a smaller context	msozeau	2007-09-21
*	Petit complément au commit 10131.	herbelin	2007-09-21
*	Correction d'un bug dans check + ajout de tests	notin	2007-09-21
*	Update on theories/Numbers	emakarov	2007-09-21
*	Update on theories/Numbers. Natural numbers are mostly complete,	emakarov	2007-09-21
*	- Fixing bug 1703 ("intros until n" falls back on the variable name when	herbelin	2007-09-21
*	Changed the definition of Nminus in BinNat.v by removing comparison.	emakarov	2007-09-20
*	Indication de quel type de constantes est dépliable dans "simpl" (cf	herbelin	2007-09-19
*	MAJ date copyright doc	herbelin	2007-09-18
*	Correction de bugs lié au commit 10124 (décalage des indices de Bruijn)	herbelin	2007-09-18
*	Raffinement de l'algorithme d'inférence de type	herbelin	2007-09-17
*	Réponse à une incompatibilité introduite dans 10114 (calcul du nombre	herbelin	2007-09-16
*	* Adding compability with ocaml 3.10 + camlp5 (rework of	letouzey	2007-09-15
*	Correction du bug #1679 (congruence) et ajout test-suite	corbinea	2007-09-14
*	Update before joining all signatures into one.	emakarov	2007-09-13
*	- renaming Qle_shift_recip_r into Qle_shift_inv_r, etc	roconnor	2007-09-07
*	errors in recdef.ml4:	bertot	2007-09-06
*	this should fix a problem described in a message by Dufourd on July 30th, 2007	bertot	2007-09-06
*	Uniformisation politique de nommage evd/isevars (evd si evar_defs,	herbelin	2007-09-06
*	Itération sur les sous-termes dans la vérification de la condition de garde	herbelin	2007-09-06
*	fixed icons	barras	2007-09-04
*	fixed icons	barras	2007-09-04
*	Utilisation d'un nouvel algorithme plus raffiné pour prendre en compte les	herbelin	2007-09-04
*	A word on the measure and wf modifiers	msozeau	2007-09-01
*	Suite commit 10103 (expansion des défs locales triviales dans l'étape	herbelin	2007-09-01
*	fin de la correction de Function	jforest	2007-08-31
*	correction bug d'efficacite dans Function	jforest	2007-08-31
*	Mise à jour des paramètres Whelp et ajouts d'options Set Whelp Server	herbelin	2007-08-30
*	Oubli dans commit 10102...	herbelin	2007-08-30
*	Prise en compte des redéfinitions de variables (définitions locales	herbelin	2007-08-29
*	- Débogueur: positionnement de set_detype_anonymous pour ne pas	herbelin	2007-08-29
*	Adding a few lemmas for reasoning about inequalities over the	roconnor	2007-08-28
*	Correction d'un bug dans check_and_warn	notin	2007-08-28
*	Oubli dans la révision 10098 (nettoyage body_of_type)	herbelin	2007-08-27