| Age | Commit message (Expand) | Author |
| 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 |
| 2000-08-08 | reparation bug des coercions (cas ou on importe une coercion faisant | barras |
| 2000-07-28 | messages d'erreur | herbelin |
| 2000-07-28 | Plus de piquants dans les actions des grammaires; nom de la grammaire pris co... | herbelin |
| 2000-07-26 | Ajout syntaxe [ phr1 ... phrn ]. pour grouper des commandes (pour Time ou Gra... | herbelin |
| 2000-07-26 | bug token "<:" et ":<" | herbelin |
| 2000-07-26 | dvips -o ==> dvips -o $@ | coq |
| 2000-07-25 | retablissement make doc et make minicoq | filliatr |
| 2000-07-24 | MAJ | herbelin |
| 2000-07-24 | Passage à des contextes de vars et de rels pouvant contenir des déclarations | herbelin |
| 2000-07-24 | Passage à des contextes de vars et de rels pouvant contenir des déclarations | herbelin |
| 2000-07-24 | Passage à des contextes de vars et de rels pouvant contenir des déclaration... | herbelin |
| 2000-07-21 | *) -> i*) | filliatr |
| 2000-07-21 | retablissement minicoq (pour Jacek) | filliatr |
| 2000-07-21 | Pattern -> parsing | delahaye |
| 2000-07-21 | Fail n + appel de interp | delahaye |
| 2000-07-21 | Modifs d'interpretation de patterns | delahaye |
| 2000-07-21 | Modifs d'interpretation de patterns + exceptions dans le lexer | delahaye |
| 2000-07-21 | Pattern -> parsing | delahaye |
| 2000-07-20 | portage Refine | filliatr |
| 2000-07-20 | tests Refine | filliatr |
| 2000-07-19 | Quelques (*i*) pour ne pas casser oczmlweb | coq |
| 2000-07-05 | Adaptation pour Alpha. | delahaye |
| 2000-07-05 | Adaptation pour alpha. | delahaye |
| 2000-07-04 | correction | mayero |
| 2000-07-03 | ajouts | mayero |
| 2000-07-03 | Opaque pas encore implementee; syntax langage tactiques | filliatr |
| 2000-07-03 | Traduction de syntaxe vers ltac | delahaye |
| 2000-07-03 | Correction de Cofix | delahaye |
| 2000-07-01 | Plus de env et sigma dans get_arity, plus de sigma dans make_arity | herbelin |
| 2000-07-01 | Précalcul de la forme canonique des constructeurs et arités pour traiter le... | herbelin |
| 2000-07-01 | Ajout fonctions sur les arités | herbelin |
| 2000-07-01 | Plus de env et sigma dans get_arity, plus de sigma dans make_arity | herbelin |
| 2000-07-01 | Précalcul de la forme canonique des constructeurs et arités pour traiter le... | herbelin |
| 2000-07-01 | Séparation des caractères spéciaux par un blanc | herbelin |
| 2000-07-01 | Retrait des parenthèses inutiles autour des tactiques | herbelin |
| 2000-07-01 | Extension de find_inductive aux co-inductifs et renommage en find_rectype | herbelin |
| 2000-07-01 | Le bon type pour list_fold_right_and_left | herbelin |
| 2000-07-01 | index devenu list_index échoue maintenant avec Not_found et plus Failure | herbelin |