| Age | Commit message (Expand) | Author |
| 2002-11-07 | Un hack camlp4 qui marche à tous les coups pour continuer à parser '(n)' co... | herbelin |
| 2002-10-23 | Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pour | herbelin |
| 2002-10-22 | Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;... | herbelin |
| 2002-10-21 | Niveau d'affichage sumor/sumbool incohérent avec le parsing | herbelin |
| 2002-10-21 | Prise en compte des délimiteurs dans les motifs de Cases | herbelin |
| 2002-10-18 | Et 48, et 80, et 81, et 91, et 95, ... pour accommoder toujours plus de contribs | herbelin |
| 2002-10-17 | Bugs dans la factorisation des règles de parsing de "{ ... } * ..." | herbelin |
| 2002-10-17 | Parsing des entiers de nat jusqu'à 29 pour accommoder certaines contribs | herbelin |
| 2002-10-14 | La règle pour parser "(1)", "(2)", ... entre en conflit avec les expressions | herbelin |
| 2002-10-13 | Mise en place d'ensembles de notations symboliques pour nat, Z et R | herbelin |
| 2002-10-13 | Nettoyage | herbelin |
| 2002-10-13 | Déplacement de + et * aux niveaux de précédence 7 et 6 | herbelin |
| 2002-10-13 | Déplacement de + et * aux niveaux de précédence 7 et 6 | herbelin |
| 2002-07-15 | Bug de précédence | herbelin |
| 2002-07-11 | Hack pour parser '{x:T|P}*B' sans parentheses | herbelin |
| 2002-05-29 | Utilisation d'Infix/Distfix autant que possible | herbelin |
| 2002-05-14 | petite erreur de syntaxe | barras |
| 2002-05-14 | ajout des theoremes eqT_rec_r et eqT_rect_r pour Rewrite | barras |
| 2002-05-07 | lemmes plus_O_n et plus_Sn_m (pour Yves) | filliatr |
| 2002-05-07 | lemmes plus_O_n et plus_Sn_m (pour Yves) | filliatr |
| 2002-04-17 | Uniformisation (Qed/Save et Implicits Arguments) | herbelin |
| 2002-02-22 | Doc | herbelin |
| 2002-02-19 | Uniformisation des theoremes dans Set et Type (def. de Acc_rect et | barras |
| 2002-02-14 | option -dump-glob pour coqdoc | filliatr |
| 2002-02-14 | Syntaxe IF then else au lieu de either and_then or_else | barras |
| 2002-01-31 | changement generation de schema d'elimination, False_rec est primitif, Constr... | mohring |
| 2002-01-29 | modification de la definition des def inductives unitaires et autorisation d'... | mohring |
| 2002-01-10 | Modifs incongrues dans le précédent commit | herbelin |
| 2002-01-09 | MAJ des Id pour coqweb | herbelin |
| 2001-11-14 | Suppression d'Export redondants | herbelin |
| 2001-10-24 | Suppression de Logic_Type.sigT, redondant avec Specif.sigT | herbelin |
| 2001-09-27 | and_rec redondant | letouzey |
| 2001-09-20 | Transparent | barras |
| 2001-09-19 | Deplacement des setoides. | clrenard |
| 2001-09-18 | Modification de l'emplacement des fichiers pour les setoides. | clrenard |
| 2001-08-30 | Fin de la modif Exc/option | mohring |
| 2001-08-29 | ajout option , Exc --> option, et lemmes dans les theories | mohring |
| 2001-08-05 | Expérimentation de NewDestruct et parfois NewInduction | herbelin |
| 2001-05-29 | Correction d'un bug du pretty-print | clrenard |
| 2001-05-15 | Modification pour passage p-automates | mohring |
| 2001-04-11 | documentation automatique de la bibliothèque standard | filliatr |
| 2001-03-30 | Introduction d'une preuve de False_rec | mohring |
| 2001-03-15 | entetes | filliatr |
| 2000-12-21 | Bug d'affichage à cause des << ... >> | herbelin |
| 2000-11-21 | separation calcul des implicites et declaration des constantes / inductifs / ... | filliatr |
| 2000-11-20 | Bug dans la règle de syntaxe de ex2 | herbelin |
| 2000-11-07 | Modification de la table des tactic Definitions pour eviter l'ecriture | mohring |
| 2000-11-07 | Changement/extension dans les noms de parseurs de Grammar | herbelin |
| 2000-10-18 | Parsing des motifs de Syntax avec la grammaire associée à l'univers de la d... | herbelin |
| 2000-07-28 | Plus de piquants dans les actions des grammaires; nom de la grammaire pris co... | herbelin |