coq - The formal proof system

Age	Commit message (Expand)	Author
2003-03-12	* empty log message *	barras
2003-01-20	Utilisation de 'Recursive' pour les tactiques récursives	herbelin
2003-01-19	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-11-14	MAJ syntaxe	herbelin
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-06-03	Protection des tactiques contre l'utilisation sans le bon contexte de thories	herbelin
2002-05-29	Fichiers contrib//.ml4 remplacent les contrib//.v	herbelin
2002-03-19	Fix d'un bug sur le test des inverses	delahaye
2002-03-17	Meilleure gestion de la reduction dans Field	delahaye
2001-12-18	Oubli d'un quote	herbelin
2001-11-14	oubli: changement de nil en nilT	mayero
2001-11-14	Changement de list en listT, cons en consT et app en appT	mayero
2001-11-05	GROS COMMIT:	barras
2001-10-23	Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR	delahaye
2001-09-21	Correction due au changement de semantique de Match	delahaye
2001-09-20	Transparent	barras
2001-08-10	Parsing	herbelin
2001-07-10	Ajout d'un Ring pour setoides	clrenard
2001-07-02	Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans Compute...	herbelin
2001-06-27	Reduction du terme preuve fourni par Field	delahaye
2001-06-27	Reduction tres significative du terme preuve	delahaye
2001-06-25	Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...	herbelin
2001-05-03	Changement de la structure des points fixes	barras
2001-04-24	Suppression d'une partie de code commente	delahaye
2001-04-20	Ajout des entetes	delahaye
2001-04-19	Ajout de Field	delahaye