aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Vers la paramétrisation des fonctions de Reduction et vers la fusion deGravatar herbelin2000-09-12
* nettoyageGravatar herbelin2000-09-10
* Correction pour make docGravatar herbelin2000-09-10
* Suppression de AbstGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path. Abstract...Gravatar herbelin2000-09-10
* Uniformisation AddPath, Print LoadPath, ... en Add Path, Print PathGravatar herbelin2000-09-10
* Intégration à TermGravatar herbelin2000-09-10
* Canonisation de certains noms dans Pretyping, Asterm et Safe_typingGravatar herbelin2000-09-06
* code mortGravatar herbelin2000-09-06
* Ajout erreur unexpected typeGravatar herbelin2000-09-06
* kernel/type_errors.mlGravatar herbelin2000-09-06
* cosmétiqueGravatar herbelin2000-08-28
* Nametab.init - bug correctedGravatar coq2000-08-21
* Bug dans le filtrage des paires, nettoyageGravatar herbelin2000-08-20
* Pattern matching de sous-termesGravatar delahaye2000-08-17
* Pattern matching de sous-termes + exceptions dans le lexerGravatar delahaye2000-08-17
* reparation bug des coercions (cas ou on importe une coercion faisantGravatar barras2000-08-08
* messages d'erreurGravatar herbelin2000-07-28
* Plus de piquants dans les actions des grammaires; nom de la grammaire pris co...Gravatar herbelin2000-07-28
* Ajout syntaxe [ phr1 ... phrn ]. pour grouper des commandes (pour Time ou Gra...Gravatar herbelin2000-07-26
* bug token "<:" et ":<"Gravatar herbelin2000-07-26
* dvips -o ==> dvips -o $@Gravatar coq2000-07-26
* retablissement make doc et make minicoqGravatar filliatr2000-07-25
* MAJGravatar herbelin2000-07-24
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Passage à des contextes de vars et de rels pouvant contenir des déclaration...Gravatar herbelin2000-07-24
* *) -> i*)Gravatar filliatr2000-07-21
* retablissement minicoq (pour Jacek)Gravatar filliatr2000-07-21
* Pattern -> parsingGravatar delahaye2000-07-21
* Fail n + appel de interpGravatar delahaye2000-07-21
* Modifs d'interpretation de patternsGravatar delahaye2000-07-21
* Modifs d'interpretation de patterns + exceptions dans le lexerGravatar delahaye2000-07-21
* Pattern -> parsingGravatar delahaye2000-07-21
* portage RefineGravatar filliatr2000-07-20
* tests RefineGravatar filliatr2000-07-20
* Quelques (*i*) pour ne pas casser oczmlwebGravatar coq2000-07-19
* Adaptation pour Alpha.Gravatar delahaye2000-07-05
* Adaptation pour alpha.Gravatar delahaye2000-07-05
* correctionGravatar mayero2000-07-04
* ajoutsGravatar mayero2000-07-03
* Opaque pas encore implementee; syntax langage tactiquesGravatar filliatr2000-07-03
* Traduction de syntaxe vers ltacGravatar delahaye2000-07-03
* Correction de CofixGravatar delahaye2000-07-03
* Plus de env et sigma dans get_arity, plus de sigma dans make_arityGravatar herbelin2000-07-01
* Précalcul de la forme canonique des constructeurs et arités pour traiter le...Gravatar herbelin2000-07-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 21:11:09 +0000