coq - The formal proof system

Age	Commit message (Expand)	Author
2009-10-21	This big commit addresses two problems:	soubiran
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-02-06	pushed evar reduction in kernel	barras
2008-03-10	fold travaille maintenant sur la forme beta-iota-zeta réduite du	herbelin
2007-06-21	Correction de plusieurs bugs de l'export XML (utilisation d'un type de	herbelin
2006-10-05	Correction de deux cas où les types inductifs n'étaient pas comparés	herbelin
2006-05-05	amelioration de la machine interpretee (vecteurs au lieu de listes d'arguments)	barras
2005-12-02	Changement des named_context	gregoire
2005-11-18	petites corrections + contournement bug projections	barras
2005-07-13	* empty log message *	barras
2005-07-12	test du tag de reduction	barras
2004-10-20	COMMITED BYTECODE COMPILER	barras
2004-07-16	Nouvelle en-tête	herbelin
2003-08-06	Ajout de l'opti des fermeture (mais debranche pour l'instant)	barras
2003-08-05	Improved reduction machine with closure: should use less memory	barras
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-08-16	Strengthenning rules for modules + No modules in sections	coq
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-01-30	cosmetique	herbelin
2001-11-29	nouvel algo de conversion plus uniforme	barras
2001-11-09	MAJ pour make doc	herbelin
2001-11-05	GROS COMMIT:	barras
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras
2001-09-20	Transparent	barras
2001-09-20	Nettoyage des commentaires	herbelin
2001-09-05	Version de la reduction dans Closure plus econome en memoire:	barras
2001-07-02	Nettoyage/restructuration des ensembles d'indicateurs de réductions	herbelin
2001-05-28	option -quality	filliatr
2001-05-03	Changement de la structure des points fixes	barras
2001-04-15	to_constr renvoie directement un constr pour contourner l'ancien Term.mk_cons...	herbelin
2001-03-23	amelioration de la consommation memoire de la conversion en eta-expansant	barras
2001-03-15	entetes	filliatr
2001-03-01	nouvelle implantation de la reduction	barras
2001-01-31	Mise en place de la possibilite d'unfolder des variables locales et des const...	filliatr
2000-12-26	Déplacement du type stack de Reduction vers Closure et utilisation pour acc�...	herbelin
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
2000-11-27	Utilisation de Let In pour les constantes locales, prise en compte des Let In...	herbelin
2000-11-24	Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametab	filliatr
2000-11-21	Ajout d'une fonction pour recuperer la liste des constantes	delahaye
2000-11-02	suppression des (* open Generic *)	filliatr
2000-10-24	Bug réduction suite modifs let-in	herbelin
2000-10-23	La réduction du Let s'appelle maintenant zeta comme dans le lambda-mu-calcul	herbelin
2000-10-04	Touche finale à la réduction du let in dans conv et closure	herbelin
2000-09-14	Minor correction for Ocamlweb + doc update	coq
2000-09-14	Nouvelle version de frterm; ajout des contextes dans l'enviornnement de rédu...	herbelin
2000-09-10	Correction pour make doc	herbelin
2000-09-10	Ajout d'un LetIn primitif.	herbelin
1999-12-01	- environment -> safe_environment	filliatr
1999-10-18	- déplacement (encore une fois !) des variables existentielles : elles sont	filliatr
1999-10-08	deplacements des var. ex. hors du noyau	filliatr