| Age | Commit message (Expand) | Author |
| 2003-11-05 | Restructuration ZArith et déport de la partie sur 'positive' dans NArith, de... | herbelin |
| 2003-11-05 | MAJ | herbelin |
| 2003-11-05 | Renommage canonique d'un lemme redondant | herbelin |
| 2003-11-05 | Branchement de Show Script sur l'afficheur structure | herbelin |
| 2003-11-05 | Amelioration de l'afficheur de script structure | herbelin |
| 2003-11-05 | maj | filliatr |
| 2003-11-04 | En v8, une notation, c'est 2 regles et un niveau | herbelin |
| 2003-11-04 | Amelioration message d'erreur | herbelin |
| 2003-11-04 | *** empty log message *** | barras |
| 2003-11-04 | Explicitation message d'erreur nombres negatifs | herbelin |
| 2003-11-04 | Pour eviter des anomalies au lieu d'erreur en mode traducteur | herbelin |
| 2003-11-04 | Extension de zarith | herbelin |
| 2003-11-04 | Amelioration message d'erreur pour ltac | herbelin |
| 2003-11-04 | Amelioration message d'erreur avec pretyping; prise en compte syntactic def d... | herbelin |
| 2003-11-04 | pour que make clean efface ide/utf8_convert.ml venant d'un .mll | letouzey |
| 2003-11-03 | Check en plus parmi les keywords | letouzey |
| 2003-11-03 | Exporting ^; utilisation arg scope implicite | herbelin |
| 2003-11-03 | Compatibilite V7.4 pour le delimiteur de positive | herbelin |
| 2003-11-03 | maj | filliatr |
| 2003-11-02 | Cosmetique | herbelin |
| 2003-11-02 | Renforcement significatif du resultat principal | herbelin |
| 2003-11-02 | Rien de bien important | herbelin |
| 2003-11-02 | Commentaires | herbelin |
| 2003-11-02 | MAJ | herbelin |
| 2003-11-02 | Le printeur de Show Script n'etait pas le bon en v7 | herbelin |
| 2003-11-02 | Typo | herbelin |
| 2003-11-02 | Ajout Diaconescu.v | herbelin |
| 2003-11-02 | AC + EXT -> EM | herbelin |
| 2003-11-02 | Relations entre le choix (forme relationnelle) avec restriction ou non | herbelin |
| 2003-11-02 | Renommage bool en boolP pour eviter la qualification | herbelin |
| 2003-11-02 | Restauration preference Rge a Rle pour compatibilite... | herbelin |
| 2003-11-02 | Restauration preference Rge a Rle pour compatibilite...; petit nettoyage | herbelin |
| 2003-11-02 | Protection contre les buts sans inegalite | herbelin |
| 2003-11-01 | Ajout CPatNotation, PrintVisibility | herbelin |
| 2003-11-01 | Extensibilite de la grammaires des patterns | herbelin |
| 2003-11-01 | Renommage Topconstr.map_aconstr_with_binders_loc | herbelin |
| 2003-11-01 | Fusion de l'univers et du nom d'entree en un 'Print Grammar entry' en v8 | herbelin |
| 2003-11-01 | Il ne faut pas mettre le constrarg des tactiques au niveau lconstr | herbelin |
| 2003-11-01 | Extensibilite de la grammaires des patterns | herbelin |
| 2003-11-01 | Traduction des noms pour les refs de pr_glob_generic (via pr_global) | herbelin |
| 2003-11-01 | Utilisation de niveaux pour l'extensibilite de la grammaires des patterns | herbelin |
| 2003-11-01 | Extension de get_constr_entry et symbol_of_production pour gerer les extensio... | herbelin |
| 2003-11-01 | Pas de defaut a 1 et LeftA pour les infixes v8; fusion de l'univers et du nom... | herbelin |
| 2003-11-01 | Ajout notations pour motifs de Cases; renommage map_aconstr_with_binders_loc | herbelin |
| 2003-11-01 | Ajout CPatNotation; renommage map_aconstr_with_binders_loc | herbelin |
| 2003-11-01 | Finalement, niveau 0 pour l'argument du '-' unaire, pour éviter que | herbelin |
| 2003-11-01 | Controle par le prefixe et plus par le nom absolu pour la recherche d'objets ... | herbelin |
| 2003-11-01 | Interdiction de nommer un object de nom commencant par Coq en dehors de la bi... | herbelin |
| 2003-11-01 | Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie... | herbelin |
| 2003-11-01 | Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie... | herbelin |