aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2000-09-10Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path. Abstract...herbelin
2000-09-10Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Pathherbelin
2000-09-10Intégration à Termherbelin
2000-09-06Canonisation de certains noms dans Pretyping, Asterm et Safe_typingherbelin
2000-09-06code mortherbelin
2000-09-06Ajout erreur unexpected typeherbelin
2000-09-06kernel/type_errors.mlherbelin
2000-08-28cosmétiqueherbelin
2000-08-21Nametab.init - bug correctedcoq
2000-08-20Bug dans le filtrage des paires, nettoyageherbelin
2000-08-17Pattern matching de sous-termesdelahaye
2000-08-17Pattern matching de sous-termes + exceptions dans le lexerdelahaye
2000-08-08reparation bug des coercions (cas ou on importe une coercion faisantbarras
2000-07-28messages d'erreurherbelin
2000-07-28Plus de piquants dans les actions des grammaires; nom de la grammaire pris co...herbelin
2000-07-26Ajout syntaxe [ phr1 ... phrn ]. pour grouper des commandes (pour Time ou Gra...herbelin
2000-07-26bug token "<:" et ":<"herbelin
2000-07-26dvips -o ==> dvips -o $@coq
2000-07-25retablissement make doc et make minicoqfilliatr
2000-07-24MAJherbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclaration...herbelin
2000-07-21*) -> i*)filliatr
2000-07-21retablissement minicoq (pour Jacek)filliatr
2000-07-21Pattern -> parsingdelahaye
2000-07-21Fail n + appel de interpdelahaye
2000-07-21Modifs d'interpretation de patternsdelahaye
2000-07-21Modifs d'interpretation de patterns + exceptions dans le lexerdelahaye
2000-07-21Pattern -> parsingdelahaye
2000-07-20portage Refinefilliatr
2000-07-20tests Refinefilliatr
2000-07-19Quelques (*i*) pour ne pas casser oczmlwebcoq
2000-07-05Adaptation pour Alpha.delahaye
2000-07-05Adaptation pour alpha.delahaye
2000-07-04correctionmayero
2000-07-03ajoutsmayero
2000-07-03Opaque pas encore implementee; syntax langage tactiquesfilliatr
2000-07-03Traduction de syntaxe vers ltacdelahaye
2000-07-03Correction de Cofixdelahaye
2000-07-01Plus de env et sigma dans get_arity, plus de sigma dans make_arityherbelin
2000-07-01Précalcul de la forme canonique des constructeurs et arités pour traiter le...herbelin
2000-07-01Ajout fonctions sur les aritésherbelin
2000-07-01Plus de env et sigma dans get_arity, plus de sigma dans make_arityherbelin
2000-07-01Précalcul de la forme canonique des constructeurs et arités pour traiter le...herbelin
2000-07-01Séparation des caractères spéciaux par un blancherbelin
2000-07-01Retrait des parenthèses inutiles autour des tactiquesherbelin
2000-07-01Extension de find_inductive aux co-inductifs et renommage en find_rectypeherbelin
2000-07-01Le bon type pour list_fold_right_and_leftherbelin
2000-07-01index devenu list_index échoue maintenant avec Not_found et plus Failureherbelin