coq - The formal proof system

Age	Commit message (Expand)	Author
2006-01-11	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...	herbelin
2005-12-02	Changement des named_context	gregoire
2005-02-06	Nettoyage et documentation de Library	herbelin
2005-02-03	Implemented a test for "Add [Semi] Setoid Ring" to check that the given	sacerdot
2005-02-03	Trivial bug fixed in "Add [Semi] Setoid Ring". An "&" in place of an "\|\|"	sacerdot
2005-02-02	setoid_rewrite t; [tac]	sacerdot
2004-11-16	Names.substitution (and related functions) and Term.subst_mps moved to	sacerdot
2004-11-16	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot
2004-09-30	cutrewrite does not work with relations that are not Coq-like equalities.	sacerdot
2004-09-29	New syntax	sacerdot
2004-09-03	The old implementation of (setoid_replace c1 with c2) used to replace	sacerdot
2004-07-23	Setoid_replace.setoid_replace: last argument (that was supposed to be	sacerdot
2004-07-22	correction d'un bug de la tactique pour les semi setoid rings.	clrenard
2004-07-16	Nouvelle en-tête	herbelin
2003-10-07	Correction du bug 335 et Export/Require Export dans un module	coq
2003-10-06	distinguer interp_cs et interp_setcs	letouzey
2003-09-28	oups	letouzey
2003-09-28	2 pbs de plus réglés concernant Setoid Ring:	letouzey
2003-09-26	Un peu plus de souplesse dans la globalisation des noms utilises par les tact...	herbelin
2003-09-22	suite (et fin) reparation Setoid Ring	letouzey
2003-09-22	tentative de rafraichissement de Setoid Ring	letouzey
2003-03-31	factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )	corbinea
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-06-19	Reparation de ring pour les setoides	clrenard
2002-06-03	Protection des tactiques contre l'utilisation sans le bon contexte de thories	herbelin
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2002-04-05	Suppression de l'application de f_equal2 pour "mult" (non inversible);	herbelin
2002-03-14	reparation semi setoid ring	clrenard
2001-12-13	compat ocaml 3.03	filliatr
2001-11-29	nouvel algo de conversion plus uniforme	barras
2001-11-05	GROS COMMIT:	barras
2001-08-10	Parsing	herbelin
2001-07-10	Ajout d'un Ring pour setoides	clrenard
2001-07-02	Nettoyage/restructuration des ensembles d'indicateurs de réductions	herbelin
2001-05-28	patch Claudio	filliatr
2001-05-14	réparation Ring (simplifications)	filliatr
2001-03-15	entetes	filliatr
2001-03-01	Déplacement de qualid dans Nametab, hors du noyau	herbelin
2001-03-01	nouvelle implantation de la reduction	barras
2001-02-16	ident au lieu de string pour le nom de base de qualid	herbelin
2001-02-14	Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...	herbelin
2001-02-05	rétablissement patch Claudio	filliatr
2001-02-02	retablissement (provisoire) de l'ancien Ring a cause d'une explosion en temps...	filliatr
2001-01-12	Comment fixed	sacerdot
2001-01-11	Now reduction to normal form is done only when the term is not	sacerdot
2001-01-11	Many unuseful rewritings are no more done by Ring.	sacerdot
2000-11-29	Nouveau long long avec Coq en tête	herbelin
2000-11-28	Prise en compte du repertoire dans le section path; utilisation de dirpath po...	herbelin