coq - The formal proof system

Age	Commit message (Expand)	Author
2003-06-14	Deplacement de le_minus de fast_integer vers Minus	herbelin
2003-06-14	Deplacement de le_minus de fast_integer vers Minus	herbelin
2003-06-14	maj	filliatr
2003-06-13	changement de spécif du fold	letouzey
2003-06-13	Ground update	corbinea
2003-06-13	CoqIDE: undo plus efficace sur les inductifs	filliatr
2003-06-13	Ground update, new files.	corbinea
2003-06-13	coqide: indentation	monate
2003-06-13	Utilisation de intro_pattern dans NewDestruct/NewInduction	herbelin
2003-06-13	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-12	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-11	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-10	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