| Age | Commit message (Expand) | Author |
| 2004-03-05 | modif des fixpoints pour que si on donne une notation au produit, les pts fix... | barras |
| 2004-03-03 | ide: silent behavior better, save icon, -byte works | marche |
| 2004-02-28 | Traduction 'Cases' en pattern-matching | herbelin |
| 2004-02-28 | Eviter la stricte redondance de regles de grammaires v7 | herbelin |
| 2004-02-26 | Keep structure information for Fixpoint declaration and Fix terms | bertot |
| 2004-02-18 | - fixed the Assert_failure error in kernel/modops | barras |
| 2004-02-17 | Ajout de lconstr, constr et binder_constr dans Print Grammar constr | herbelin |
| 2004-02-13 | Correction d'un pb '{ _ }' et uniformisation du comportement de Notation et R... | herbelin |
| 2004-02-12 | Localisation des erreurs d'internalisation des notations de tactiques | herbelin |
| 2004-02-12 | Localisation des erreurs d'internalisation des notations de tactiques | herbelin |
| 2004-02-12 | Décomposition automatique des règles d'analyse syntaxique pour les | herbelin |
| 2004-02-04 | Boite autour des quote pour eviter un retour a la ligne apres le premier guil... | herbelin |
| 2004-02-04 | search window | coq |
| 2004-02-03 | Bug focus | herbelin |
| 2004-02-03 | Protection contre noms de variable indefinis et guillemets autour des constr | herbelin |
| 2004-01-29 | Ajout option raw_print (Set Printing All) pour desactiver toute fonctionnalit... | herbelin |
| 2004-01-29 | Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :... | herbelin |
| 2004-01-26 | reparation de qqs bugs du traducteur | barras |
| 2004-01-22 | Protection table des locations lors de Load (pour coqdoc) | herbelin |
| 2004-01-21 | Export information des references de notations pour coqdoc | herbelin |
| 2004-01-15 | Ajout nouvelles options | herbelin |
| 2004-01-15 | Ajout load-vernac-source-verbose | herbelin |
| 2004-01-13 | Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a... | herbelin |
| 2004-01-09 | bugs avec Pose et Assert | barras |
| 2004-01-05 | Defaut d'information affichage en cas de notation incompatible | herbelin |
| 2004-01-02 | meilleure presentation des commentaires du traducteur | barras |
| 2003-12-30 | ameliorations coqide | coq |
| 2003-12-24 | *** empty log message *** | barras |
| 2003-12-20 | MAJ messages d'erreurs en accord avec la doc | herbelin |
| 2003-12-20 | Bug rattrapage erreur locate_reference | herbelin |
| 2003-12-19 | Suppression de l'espace avant les notations commencant par un ident | herbelin |
| 2003-12-12 | option -n de coq-tex | marche |
| 2003-11-29 | Deplacement des fichiers ancienne syntaxe dans theories7, contrib7 et states7... | herbelin |
| 2003-11-29 | Deplacement des fichiers ancienne syntaxe dans theories7, contrib7 et states7... | herbelin |
| 2003-11-29 | Utilisation nom dans message d'erreur implicite pas trouve | herbelin |
| 2003-11-27 | Monstrueuse inefficacite due a l'innocence du redacteur de la ligne vis a vis... | herbelin |
| 2003-11-22 | Traitement plus clair, notamment pour Locate, de quand quoter les composantes... | herbelin |
| 2003-11-21 | MAJ format et doc | herbelin |
| 2003-11-18 | Bug: faut brancher la sortie des tactiques sur stdout pendant traduction | herbelin |
| 2003-11-18 | Utilisation de la date cvs dans l'en-tete si make.result existe | herbelin |
| 2003-11-15 | Bug v8 (regles connues etaient re-enregistrees) + tables dans egrammar | herbelin |
| 2003-11-15 | Ajout Print Implicit avec depliage du type | herbelin |
| 2003-11-14 | Check bavard meme en mode silencieux, car on l'a voulu | herbelin |
| 2003-11-12 | Prise en compte des alias syntaxiques vers des references dans divers lieux d... | herbelin |
| 2003-11-12 | Idtac peut prendre un argument à afficher | narboux |
| 2003-11-12 | petits changements de syntaxe | barras |
| 2003-11-10 | Re-suppression de is_verbose dans Print, pour coqide | herbelin |
| 2003-11-10 | Suppression SearchNamed finalement redondant avec SearchAbout | herbelin |
| 2003-11-09 | Mise en place traduction des tactiques apres evaluation pour permettre des ch... | herbelin |
| 2003-11-08 | Fusion de tuple_constr/tuple_pattern dans operconstr/pattern | herbelin |