aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction/extract_env.mli
AgeCommit message (Expand)Author
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
2008-11-06Cosmetic: no more whitespace at end of lines in extraction filesletouzey
2008-05-07export Extract_env.mono_environment in the mli letouzey
2007-10-17Major reorganisation of the extraction "backend".letouzey
2004-07-16Nouvelle en-têteherbelin
2003-11-10essai d'extraction sous un moduleletouzey
2003-11-09factorisation de (recursive) libraryletouzey
2003-04-16BIG MAJ Extraction:letouzey
2003-01-22Extraction des modules, enfin !letouzey
2002-12-13debut de parcours des modulesletouzey
2002-12-05code cleanup (+ debut de commencement de modules)letouzey
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-08-02Modules dans COQ\!\!\!\!coq
2002-07-16Gros Remaniement Extraction:letouzey
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2001-04-04rollback sur les commandes Extract Constant/Inductive; nettoyage et documenta...filliatr
2001-03-28changement type_var et signaturefilliatr
2001-03-27extraction recursive d'un morceau d'environnementfilliatr