aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction
Commit message (Expand)AuthorAge
* les modifs depuis la 7.4Gravatar letouzey2003-11-12
* TODOGravatar letouzey2003-11-12
* Extraction Module M devient simplement Extraction MGravatar letouzey2003-11-12
* le pb du <<.v vu comme module>> engendre maintenant une erreurGravatar letouzey2003-11-10
* message informant de l'ecriture d'un fichier extraitGravatar letouzey2003-11-10
* révision du traitement des axiomes non réalisésGravatar letouzey2003-11-10
* essai d'extraction sous un moduleGravatar letouzey2003-11-10
* factorisation de (recursive) libraryGravatar letouzey2003-11-09
* changement nouvelle syntaxe (pt fixes)Gravatar barras2003-10-10
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
* pour ocamlwebGravatar letouzey2003-10-06
* Cacher les .v8Gravatar herbelin2003-10-03
* traducteur: affiche les commentaires a l'interieur des commandesGravatar barras2003-09-22
* bug dans calcul nb d'occurrencesGravatar letouzey2003-09-05
* correction d'un stack overflow possible (PR#320)Gravatar letouzey2003-08-28
* Traduction mlnamesGravatar herbelin2003-08-14
* bug typage du cases/identity: optim off si inductif avec varsGravatar letouzey2003-07-10
* renommage des modules 1er niveau en monolithiqueGravatar letouzey2003-07-10
* bug match matchGravatar letouzey2003-07-08
* enieme correction du nommage modulaireGravatar letouzey2003-06-12
* fin de l'affichage des signatures de modules dans les *.mlGravatar letouzey2003-06-12
* interaction entre fun/case permut et assert falseGravatar letouzey2003-06-08
* oupsGravatar letouzey2003-05-30
* := dans un record engendre un LetIn qui n'etait pas géréGravatar letouzey2003-05-29
* gestion plus fine des beta-redex lineaires (cf nb_occur_match)Gravatar letouzey2003-05-28
* bug concernant les projecteurs de Record avec args logiquesGravatar letouzey2003-04-28
* adaptation a Acc_iterGravatar letouzey2003-04-28
* OoopsGravatar letouzey2003-04-17
* temporaireGravatar letouzey2003-04-17
* BIG MAJ Extraction:Gravatar letouzey2003-04-16
* Extract Constant marche avec les axiomes schémas de typesGravatar letouzey2003-03-25
* pour coq-ideGravatar letouzey2003-03-11
* pour ocamlwebGravatar letouzey2003-03-11
* bugs/améliorations trouvés via FTAGravatar letouzey2003-02-21
* maj status de l'extraction des modulesGravatar letouzey2003-02-03
* hack horrible pour renommage dans Modules Types et FuncteursGravatar letouzey2003-02-03
* encore un long_knGravatar letouzey2003-02-03
* plus d'environment fixe cur_env mais un environment evolutifGravatar letouzey2003-02-02
* fignolageGravatar letouzey2003-01-30
* pb d'hier resolu. RecommitGravatar letouzey2003-01-30
* apres le backtrack precedent, remise de trois points precis et sursGravatar letouzey2003-01-29
* Ca a tout pété -> Bactrack a la version d'hierGravatar letouzey2003-01-29
* affichage module et module typeGravatar letouzey2003-01-29
* affichage module et module typeGravatar letouzey2003-01-29
* affichage module et module typeGravatar letouzey2003-01-29
* workaround en attendant traitement reel des modules typesGravatar letouzey2003-01-28
* amelioration du pretty-print des modulesGravatar letouzey2003-01-28
* nouvelle gestion des constantes de typeGravatar letouzey2003-01-28
* oubli des add_recursors singleton logiquesGravatar letouzey2003-01-23
* maj V7.4Gravatar letouzey2003-01-23