aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction
Commit message (Expand)AuthorAge
* Modules et Records: gros changements pour prendre en compte le nouveau mind_r...Gravatar letouzey2004-06-28
* correspondance des records et noms de champs de records entre un module et sa...Gravatar letouzey2004-06-25
* correction rapide du bug PR\#592Gravatar letouzey2004-04-05
* me = andouilleGravatar letouzey2004-03-25
* Selon les optims, le let-in peut avoir maintenant des argsGravatar letouzey2004-03-25
* nouvelle commande Set Extraction Flag: reglage fins des optimsGravatar letouzey2004-03-24
* meme correction de bug, en moins bourrinGravatar letouzey2004-03-23
* PolyList -> ListGravatar letouzey2004-03-22
* correction d'un bug faisant inliner minus, mult, ...Gravatar letouzey2004-03-22
* petit rajeunissement du test d'extractionGravatar letouzey2004-03-20
* Mise en place temporaire d'un afficheur de 'language' pour le traducteurGravatar herbelin2004-03-13
* petit bug avec Extraction OptimizeGravatar letouzey2004-02-13
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* 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