coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	fcts tail-recursives	filliatr	2003-06-13
*	Require Export	filliatr	2003-06-13
*	install-fsets	filliatr	2003-06-13
*	FSets, mais pas compile' par make world	filliatr	2003-06-13
*	suite changements ZArith en vu de librairie FSet	letouzey	2003-06-13
*	quelques adaptations de Zarith en vu de la nouvelle librarie FSet	letouzey	2003-06-13
*	coqide: about now displays versions/Fix for alt-enter	monate	2003-06-13
*	Deplacement d'un lemme sur nat de ZArith vers Arith	herbelin	2003-06-13
*	CoqIDE: undo immediat sur les commandes ne modifiant pas l'etat	filliatr	2003-06-13
*	Ground update.	corbinea	2003-06-13
*	enieme correction du nommage modulaire	letouzey	2003-06-12
*	fin de l'affichage des signatures de modules dans les *.ml	letouzey	2003-06-12
*	MAJ	herbelin	2003-06-12
*	INZ reste constante pour compat V7 mais Unfold INZ est supprimé par le tradu...	herbelin	2003-06-12
*	Ajout option translate_syntax pour caractériser l'interprétation du traduct...	herbelin	2003-06-12
*	Pb quand une meme classe est definie dans 2 fichiers	herbelin	2003-06-11
*	Token '.(' seulement pour v8, sinon conflit avec '.(*'	herbelin	2003-06-11
*	maj	filliatr	2003-06-11
*	MAJ	herbelin	2003-06-10
*	Typo	herbelin	2003-06-10
*	Module Bij inutilise	herbelin	2003-06-10
*	Import nat_scope	herbelin	2003-06-10
*	Suppression d'une occurrence superflue d'argument de type dans Notation sacha...	herbelin	2003-06-10
*	Deplacement delimiteur T dans Notations	herbelin	2003-06-10
*	Module Bij inutilise	herbelin	2003-06-10
*	Ajout notation c.(f) en v8 pour les projections de Record	herbelin	2003-06-10
*	freshid -> fresh	herbelin	2003-06-10
*	Déplacement traducteur de nom dans Constrextern pour accès aux noms longs	herbelin	2003-06-10
*	Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur de...	herbelin	2003-06-10
*	Simplification case_info	herbelin	2003-06-10
*	Ajout notation c.(f) en v8 pour les projections de Record; raffinement divers	herbelin	2003-06-10
*	Raffinement divers	herbelin	2003-06-10
*	Globalisation des tactiques avant traduction pour capture des noms; affinemen...	herbelin	2003-06-10
*	Distinction mode v7 ou translate; conséquences du déplacement traducteur de...	herbelin	2003-06-10
*	Déplacement de code dans command; MAJ DebugOn	herbelin	2003-06-10
*	Mise en place structure pour des 'arguments scope' dirigés par une classe	herbelin	2003-06-10
*	Amélioration afficheur de Cases pour les constr_pattern	herbelin	2003-06-10
*	Passage des noms de tactiques à kernel_name pour compatibilité avec les fon...	herbelin	2003-06-10
*	Déplacement traducteur de nom dans Constrextern pour accès aux noms longs	herbelin	2003-06-10
*	Ajout notation c.(f) en v8 pour les projections de Record	herbelin	2003-06-10
*	Factorisation de detype_case pour utilisation par l'afficheur de pattern	herbelin	2003-06-10
*	Traducteur + passage des noms de tactiques à kernel_name pour compatibilité...	herbelin	2003-06-10
*	Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur de...	herbelin	2003-06-10
*	Amélioration afficheur de Cases pour les constr_pattern	herbelin	2003-06-10
*	Extension de Locate sur les symboles avec recherche de sous-chaînes; mise en...	herbelin	2003-06-10
*	Globalisation de ce qui n'etait pas encore globalise	herbelin	2003-06-10
*	code mort	herbelin	2003-06-10
*	Ajout fonctions de recherche de sous-chaines (merci a Jacek)	herbelin	2003-06-10
*	maj	filliatr	2003-06-09
*	interaction entre fun/case permut et assert false	letouzey	2003-06-08