coq - the Coq proof assistant

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