aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2000-11-06nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...filliatr
2000-11-05Nouveau mode de compilation de .ml4herbelin
2000-11-05Déplacement d'une partie de g_vernac.ml4 dans g_proofs.ml4 car fichier deven...herbelin
2000-11-03compilation des fichiers ml4 sans GNUseriesfilliatr
2000-11-02suppression des (* open Generic *)filliatr
2000-10-31- simplification Makefile (compilation des fichiers .ml'; pas encore parfaitfilliatr
2000-10-30Priorite du Try/Orelse + Debug switch + correction bug dans Patterndelahaye
2000-10-26Renommage var en named et decl en assumherbelin
2000-10-24Bug de copier-collerherbelin
2000-10-21Pb affichage warningherbelin
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec sorts)...herbelin
2000-10-18Renommage canonique :herbelin
2000-10-18Parsing des motifs de Syntax avec la grammaire associée à l'univers de la d...herbelin
2000-10-182èmeherbelin
2000-10-18Mise en place de parseurs avec globalisation pas seulement dans les quotation...herbelin
2000-10-18Nettoyageherbelin
2000-10-18globalize_command devient globalize_constrherbelin
2000-10-18Correction pb de globalisation dans print_mutualherbelin
2000-10-17Pb factorisation de Print Grammarherbelin
2000-10-16Changement "command" en "constr" et globalize_command en globalize_constrherbelin
2000-10-11Suite du précédentherbelin
2000-10-10Plus d'échec sur les globaux lorsque prterm est appelé par le débuggerherbelin
2000-10-06Correction incompatibilites dans la fn des types des inductifsherbelin
2000-10-05Bug affichage des implicites; bug de compatibilité LAMBDA/LAMBDALISTherbelin
2000-10-04Utilisation de local_strong plutôt que strong buggé avec défs localesherbelin
2000-10-03Ajout castedopenconstrargherbelin
2000-10-03Ajout de globpr dans tacprherbelin
2000-10-03Ajout castedopenconstrarg; Renommage tactique Let en LetTacherbelin
2000-10-03Reorganisation des interp_constrherbelin
2000-10-01Renommage AppL en Appherbelin
2000-10-01Disparition du type oper mais nouveau type global_referenceherbelin
2000-10-01Déplacement 'a reference et binder_kind de Term vers Rawtermherbelin
2000-09-26Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...herbelin
2000-09-14Abstraction de constrherbelin
2000-09-12Modification mkAppL; abstraction via kind_of_term; changement dans Reductionherbelin
2000-09-10Correction pour make docherbelin
2000-09-10Suppression de Abstherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-09-06Canonisation de certains noms dans Pretyping, Asterm et Safe_typingherbelin
2000-09-06code mortherbelin
2000-08-20Bug dans le filtrage des paires, nettoyageherbelin
2000-08-17Pattern matching de sous-termes + exceptions dans le lexerdelahaye
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-25retablissement make doc et make minicoqfilliatr
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-07-21retablissement minicoq (pour Jacek)filliatr
2000-07-21Pattern -> parsingdelahaye
2000-07-21Modifs d'interpretation de patterns + exceptions dans le lexerdelahaye
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-16 01:58:48 +0000