aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction/extract_env.ml
AgeCommit message (Expand)Author
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
2009-01-23Petit nettoyage faisant suite au commit #11847 .aspiwack
2009-01-22Fix #2011 : an incorrect environment when extracting Module ... with ...letouzey
2009-01-22Extraction Library works now when some files share the same short name (fix #...letouzey
2008-12-17Avoid printing that extraction has created file Foo when it's not the caseletouzey
2008-12-16Extraction Blacklist : a new command for avoiding conflicts with existing filesletouzey
2008-12-16Extraction: also comply to Set Printing Width when producing external 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-10-16Extraction of Module with eq = ... : fix for bug #1853letouzey
2008-10-16Attempt to clarify Extract_env.extract_seb_specletouzey
2008-10-15Report des commits 11417 et 11437 de la v8.2soubiran
2008-04-15fix some bogus calls to id_of_string by the extractionletouzey
2008-03-14Ajout des alias de module dans le noyau.soubiran
2008-03-05Attempt of fix for extraction of modules typesletouzey
2008-02-01Beaoucoup de changements dans la representation interne des modules.soubiran
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
2007-10-21An error message instead of an empty extraction when the monolithic letouzey
2007-10-17Repair Haskell/Scheme extraction in the new extraction backend design: 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-01-12Suite au mail de Lionel a propos du Makefile: letouzey
2006-10-28Extension du polymorphisme de sorte au cas des définitions dans Type.herbelin
2004-11-18When a reference to a constructor is met its inductive type must be closed.sacerdot
2004-11-16Names.substitution (and related functions) and Term.subst_mps moved tosacerdot
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
2004-07-16Nouvelle en-têteherbelin
2003-11-12Extraction Module M devient simplement Extraction Mletouzey
2003-11-10le pb du <<.v vu comme module>> engendre maintenant une erreurletouzey
2003-11-10essai d'extraction sous un moduleletouzey
2003-11-09factorisation de (recursive) libraryletouzey
2003-10-06pour ocamlwebletouzey
2003-04-16BIG MAJ Extraction:letouzey
2003-02-02plus d'environment fixe cur_env mais un environment evolutifletouzey
2003-01-29apres le backtrack precedent, remise de trois points precis et sursletouzey
2003-01-29Ca a tout pété -> Bactrack a la version d'hierletouzey
2003-01-29affichage module et module typeletouzey
2003-01-22Extraction des modules, enfin !letouzey
2003-01-09Export M + Module M <: SIGcoq
2002-12-13debut de parcours des modulesletouzey
2002-12-09chamboulement du codage des indcutifs extraits; deplacements des tables; ...letouzey
2002-12-05reorganisation des recherches de ref dans ml_declletouzey
2002-12-05code cleanup (+ debut de commencement de modules)letouzey
2002-11-28Remaniement du pp, suite: vers un renommage modulaire correcteletouzey
2002-10-31L'extraction c'est magic cvs -n upletouzey
2002-09-24suite chgt liés aux modulesletouzey
2002-08-02Modules dans COQ\!\!\!\!coq
2002-07-24reparation d'un bug (dummy_lams -> anonym_lams) + chgmt structutr d'un ml_typeletouzey
2002-07-16Gros Remaniement Extraction:letouzey