aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction/table.mli
AgeCommit message (Expand)Author
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
2009-01-22Extraction Library works now when some files share the same short name (fix #...letouzey
2008-12-16Extraction Blacklist : a new command for avoiding conflicts with existing filesletouzey
2008-11-06Cosmetic: no more whitespace at end of lines in extraction filesletouzey
2008-11-05Better extraction renaming phase (fix #1914 plus other non-reported bugs)letouzey
2008-10-21warning message when a qualid to extract can be both a module or a cstletouzey
2008-07-20Extraction: better dependency computation (after optimisations)letouzey
2007-10-21An error message instead of an empty extraction when the monolithic letouzey
2007-10-17Major reorganisation of the extraction "backend".letouzey
2007-10-09Extraction now checks that the required libraries are indeed loaded (bug #1144)letouzey
2007-10-09Extract Inline/Inductive/Constant can now be used from inside a moduleletouzey
2007-10-08Better use of tables for storing results of extract_ind (bug #1709)letouzey
2004-12-09travail sur les types extraitsletouzey
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
2004-07-16Nouvelle en-têteherbelin
2004-06-28Modules et Records: gros changements pour prendre en compte le nouveau mind_r...letouzey
2004-03-24nouvelle commande Set Extraction Flag: reglage fins des optimsletouzey
2003-11-10le pb du <<.v vu comme module>> engendre maintenant une erreurletouzey
2003-11-10révision du traitement des axiomes non réalisésletouzey
2003-11-10essai d'extraction sous un moduleletouzey
2003-04-28bug concernant les projecteurs de Record avec args logiquesletouzey
2003-04-16BIG MAJ Extraction:letouzey
2003-03-25Extract Constant marche avec les axiomes schémas de typesletouzey
2003-02-21bugs/améliorations trouvés via FTAletouzey
2003-02-02plus d'environment fixe cur_env mais un environment evolutifletouzey
2003-01-22Extraction des modules, enfin !letouzey
2002-12-09chamboulement du codage des indcutifs extraits; deplacements des tables; ...letouzey
2002-12-05code cleanup (+ debut de commencement de modules)letouzey
2002-11-28Remaniement du pp, suite: vers un renommage modulaire correcteletouzey
2002-11-26debut de support des records camlletouzey
2002-11-25cleanup table.ml + erreur si Extraction Inline sous sectionletouzey
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-10-31L'extraction c'est magic cvs -n upletouzey
2002-08-02Modules dans COQ\!\!\!\!coq
2002-07-16Gros Remaniement Extraction:letouzey
2002-06-07extraction vers schemeletouzey
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-03-04Big commit extraction:letouzey
2001-11-05GROS COMMIT:barras
2001-10-26Fin de mise en place de l'option Optimize. Reorganisation du pretty-print. ET...letouzey
2001-10-22chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les o...letouzey