aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction/table.ml
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-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
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-09forbid extraction under a module typeletouzey
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
2006-10-28Extension du polymorphisme de sorte au cas des définitions dans Type.herbelin
2006-10-04Correction bug #1211notin
2005-01-03HUGE COMMITsacerdot
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-25me = andouilleletouzey
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-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
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-08-02Modules dans COQ\!\!\!\!coq
2002-07-16petit bug lors du passage d'hugoletouzey
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-11Factorisation de la grammaire pour Extraction Language.letouzey
2002-03-05cas des constructeurs singletons. Messages d'erreur. Revision de test_extract...letouzey
2002-03-04Big commit extraction:letouzey
2001-12-18ote les redondances des entetesletouzey
2001-12-13compat ocaml 3.03filliatr
2001-11-14Revolution culturelle: suppression des arguments propletouzey
2001-11-05GROS COMMIT:barras