coq - The formal proof system

Age	Commit message (Expand)	Author
2003-01-16	Bugs affichage	herbelin
2003-01-16	-emacs: plus de prompt entre les lignes	filliatr
2003-01-15	Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...	herbelin
2003-01-09	Export M + Module M <: SIG	coq
2003-01-06	SearchAbout	filliatr
2002-12-31	Amélioration règles d'affichage	herbelin
2002-12-21	Légère amélioration des messages d'erreur des with-bindings et des Rewrite	herbelin
2002-12-21	Affinement affichage	herbelin
2002-12-19	Petit netoyage dans lib	coq
2002-12-19	suite du commit precedent	barras
2002-12-15	Prise en compte des scopes traversés dans les notations	herbelin
2002-12-12	Ajout du vernac Proof with	gregoire
2002-12-10	Ajout options -v7 et -v8, et commandes V7only et V8only	herbelin
2002-12-10	Ajout options -v7 et -v8, et commandes V7only et V8only	herbelin
2002-12-09	Problèmes et améliorations divers affichage	herbelin
2002-12-09	Code mort ?	herbelin
2002-12-04	Correction divers bugs d'affichage; explicitation du niveau de grammaire quan...	herbelin
2002-12-04	Correction divers bugs d'affichage; explicitation du niveau de grammaire quan...	herbelin
2002-12-04	Modification Require From	mohring
2002-12-03	la table PARAMETER n'existe plus (mergé dans la table CONSTANT)	letouzey
2002-12-03	Préparation à la prise en compte des changements de scopes internes aux not...	herbelin
2002-12-03	Pas de globalisation impérative pour les Grammar	herbelin
2002-12-02	Re-déplacement du résultat de Grammar au niveau constr_expr (globalisation ...	herbelin
2002-12-02	Ajout des options "Set Contextual Implicits" et "Set Strict Implicits	herbelin
2002-12-02	On force l'associativité pour les entrées sans niveaux	herbelin
2002-11-29	Raffinement syntaxe Infix	herbelin
2002-11-28	Affinement de la gestion des niveaux toujours; type ETBigint	herbelin
2002-11-28	typo ?	letouzey
2002-11-28	Affinement encore	herbelin
2002-11-27	Ajout répertoire interp	herbelin
2002-11-26	Réaffichage des Syntactic Definition (printer constr_expr).	herbelin
2002-11-25	Syntaxe delimiteurs	herbelin
2002-11-25	MAJ delimiters et niveaux d'associativite	herbelin
2002-11-24	Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...	herbelin
2002-11-19	Autoriser les abbreviations de Cases	herbelin
2002-11-15	Passage à une représentation des fixpoints plus primitive dans constr_expr ...	herbelin
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-11-06	Un Local construit par preuve hors section doit être considéré global	herbelin
2002-11-05	Intégration des modifs de la branche mowgli :	herbelin
2002-11-05	Nouvelle option -xml à coqtop pour compiler un développement en	herbelin
2002-10-30	Optimisation du choix des niveaux intermédiaires dans une notation complexe	herbelin
2002-10-26	code mort	herbelin
2002-10-23	Clarification changements autour de Remark/Fact/Local	herbelin
2002-10-23	Le test de redondance d'une règle était trop fort	herbelin
2002-10-22	Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;...	herbelin
2002-10-21	Prise en compte des délimiteurs dans les motifs de Cases	herbelin
2002-10-16	Réparation du mécanisme des infixes quand ils commencent par une lettre	herbelin
2002-10-14	Meilleure analyse de si une règle de grammaire/syntaxe existent déjà ou pas	herbelin
2002-10-14	Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'une	herbelin
2002-10-13	Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...	herbelin