coq - The formal proof system

Age	Commit message (Expand)	Author
2007-10-02	Report des modifications faites sur le configure en r10039, r10052, r10053 et...	notin
2007-10-02	Now NMake is proved	thery
2007-10-02	Correcting error message when adding Setoid, Relation or morphism (bug #1626)	jforest
2007-10-01	Added the compilation of theories/Numbers to Makefile.common. The following t...	emakarov
2007-10-01	Nouvelle mise à jour	herbelin
2007-10-01	Amendement à la révision 10124 : déplacement de apprec_nohdbeta entre	herbelin
2007-10-01	Complément nécessaire aux révisions 10156 et 10157	herbelin
2007-09-30	Suite de 10157	herbelin
2007-09-30	Ajout infos de débogage de "universe inconsistency" quand option Set	herbelin
2007-09-28	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-27	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-26	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-25	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-24	Added the documentation for Backtrack and BackTo.	courtieu
2007-09-21	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-20	Changed the definition of Nminus in BinNat.v by removing comparison.	emakarov
2007-09-19	Indication de quel type de constantes est dépliable dans "simpl" (cf	herbelin
2007-09-18	MAJ date copyright doc	herbelin
2007-09-18	Correction de bugs lié au commit 10124 (décalage des indices de Bruijn)	herbelin
2007-09-17	Raffinement de l'algorithme d'inférence de type	herbelin
2007-09-16	Réponse à une incompatibilité introduite dans 10114 (calcul du nombre	herbelin
2007-09-15	* Adding compability with ocaml 3.10 + camlp5 (rework of	letouzey
2007-09-14	Correction du bug #1679 (congruence) et ajout test-suite	corbinea
2007-09-13	Update before joining all signatures into one.	emakarov
2007-09-07	- renaming Qle_shift_recip_r into Qle_shift_inv_r, etc	roconnor
2007-09-06	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-04	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-01	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-08-31	fin de la correction de Function	jforest