coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	La notation with dependante + affichage dependante de moduels corrige	coq	2002-09-20
*	maj	filliatr	2002-09-20
*	maj	filliatr	2002-09-20
*	maj	filliatr	2002-09-20
*	portage Correctness (substitutivité pour les modules)	filliatr	2002-09-19
*	retablissement de Correctness (pas encore teste' cependant)	filliatr	2002-09-18
*	echappements incorrects dans chaine	filliatr	2002-09-17
*	Réintroduction de l'expansion des variables de shell et de '~' dans les	herbelin	2002-09-16
*	Un peu plus de flexibilité pour la position du '.' final	herbelin	2002-09-16
*	Subst (tout court)	filliatr	2002-09-16
*	Ajout contribs manquantes	herbelin	2002-09-13
*	tactique Subst x1 ... xn	filliatr	2002-09-11
*	Code mort de AutoRewrite	herbelin	2002-09-09
*	Amélioration messages d'erreur non inférence implicites	herbelin	2002-09-03
*	pretyping/pretyping.ml	herbelin	2002-09-03
*	Correction	coq	2002-08-21
*	La notation 'with'. L'interpretation - version preliminaire	coq	2002-08-19
*	MAJ .depend	coq	2002-08-19
*	Pretty-printing preliminaire des modules, commandes	coq	2002-08-19
*	Suppression automatique du corps des définitions locales opaques dans	herbelin	2002-08-17
*	correction de bugs:	barras	2002-08-16
*	Encore quelques tests sur modules...	coq	2002-08-16
*	Strengthenning rules for modules + No modules in sections	coq	2002-08-16
*	Test for redundant clauses	herbelin	2002-08-15
*	Test affichage optimal des coercions	herbelin	2002-08-14
*	MAJ depend.coq	coq	2002-08-14
*	AutoRewrite substitutive...	coq	2002-08-13
*	Renoncement à distinguer les types "constr" et "types"; nettoyage	herbelin	2002-08-13
*	Renoncement à distinguer les types "constr" et "types"; nettoyage	herbelin	2002-08-13
*	Renoncement	herbelin	2002-08-13
*	Petites corrections ici et la	coq	2002-08-13
*	Preuves dans CC de	herbelin	2002-08-13
*	En attendant la 3.06, remplacement de +camlp4 par CAMLLIB/camlp4	herbelin	2002-08-02
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	MAJ pour TAF	desmettr	2002-07-31
*	Theoreme des accroissements finis generalises et corollaires	desmettr	2002-07-31
*	* empty log message *	desmettr	2002-07-31
*	MAJ pour Exp_prop	desmettr	2002-07-31
*	Proprietes de l'exponentielle	desmettr	2002-07-31
*	* empty log message *	desmettr	2002-07-31
*	Réparation d'un bug qui considérait les composantes d'un QUALID	herbelin	2002-07-30
*	Branchement de Assert, Pose et LetTac sur l'algo de création de noms	herbelin	2002-07-30
*	MAJ pour Rtrigo_reg	desmettr	2002-07-29
*	Regularite de sin et cos	desmettr	2002-07-29
*	Continuite des series de fonctions NC	desmettr	2002-07-29
*	* empty log message *	desmettr	2002-07-29
*	Ajout d'un point d'entree pour exporter les arbres de preuves en XML	herbelin	2002-07-24
*	reparation d'un bug (dummy_lams -> anonym_lams) + chgmt structutr d'un ml_type	letouzey	2002-07-24
*	suppression des ./ dans les noms des librairies	barras	2002-07-24
*	MAJ commentaires	herbelin	2002-07-23