| Age | Commit message (Expand) | Author |
| 2000-10-01 | Plus de whd_castapp | herbelin |
| 2000-10-01 | Chasse aux de-cast inutiles | herbelin |
| 2000-10-01 | renommage map_constr_with_named_binders | herbelin |
| 2000-10-01 | Plus de whd_castapp | herbelin |
| 2000-10-01 | Plus de whd_castapp_stack | herbelin |
| 2000-10-01 | renommage map_constr_with_named_binders | herbelin |
| 2000-10-01 | Passage de la structure DOPN, DOP2, ... à une structure exprimant directemen... | herbelin |
| 2000-10-01 | Disparition du type oper mais nouveau type global_reference | herbelin |
| 2000-10-01 | Déplacement 'a reference et binder_kind de Term vers Rawterm | herbelin |
| 2000-10-01 | Code mort | herbelin |
| 2000-10-01 | Elimination de coupures... | herbelin |
| 2000-09-26 | Retrait de whd_ise1_metas | herbelin |
| 2000-09-26 | Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d... | herbelin |
| 2000-09-26 | MAJ | herbelin |
| 2000-09-18 | mise a jour dependances | filliatr |
| 2000-09-15 | On laisse les LetIn dans les types des constructeurs et des éliminations | herbelin |
| 2000-09-15 | Commentaires | herbelin |
| 2000-09-15 | Messages d'erreurs | herbelin |
| 2000-09-15 | Expression anglaise | herbelin |
| 2000-09-14 | Minor correction for Ocamlweb + doc update | coq |
| 2000-09-14 | Bugs parenthèses | herbelin |
| 2000-09-14 | MAJ | herbelin |
| 2000-09-14 | Suppression Redinfo Sosub Abstraction | herbelin |
| 2000-09-14 | Abstraction de constr | herbelin |
| 2000-09-14 | Déplacement de fonctions de Reduction vers Tacred | herbelin |
| 2000-09-14 | Nouvelle version de frterm; ajout des contextes dans l'enviornnement de rédu... | herbelin |
| 2000-09-14 | Intégré à Tacred | herbelin |
| 2000-09-14 | Rendus obsolètes par le LetIn | herbelin |
| 2000-09-14 | Abstraction de constr | herbelin |
| 2000-09-12 | MAJ | herbelin |
| 2000-09-12 | Modification mkAppL; abstraction via kind_of_term; changement dans Reduction | herbelin |
| 2000-09-12 | Vers la paramétrisation des fonctions de Reduction et vers la fusion de | herbelin |
| 2000-09-10 | nettoyage | herbelin |
| 2000-09-10 | Correction pour make doc | herbelin |
| 2000-09-10 | Suppression de Abst | herbelin |
| 2000-09-10 | Ajout d'un LetIn primitif. | herbelin |
| 2000-09-10 | Ajout d'un LetIn primitif. | herbelin |
| 2000-09-10 | Ajout d'un LetIn primitif. | herbelin |
| 2000-09-10 | Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path. Abstract... | herbelin |
| 2000-09-10 | Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path | herbelin |
| 2000-09-10 | Intégration à Term | herbelin |
| 2000-09-06 | Canonisation de certains noms dans Pretyping, Asterm et Safe_typing | herbelin |
| 2000-09-06 | code mort | herbelin |
| 2000-09-06 | Ajout erreur unexpected type | herbelin |
| 2000-09-06 | kernel/type_errors.ml | herbelin |
| 2000-08-28 | cosmétique | herbelin |
| 2000-08-21 | Nametab.init - bug corrected | coq |
| 2000-08-20 | Bug dans le filtrage des paires, nettoyage | herbelin |
| 2000-08-17 | Pattern matching de sous-termes | delahaye |
| 2000-08-17 | Pattern matching de sous-termes + exceptions dans le lexer | delahaye |