aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction/extract_env.ml
AgeCommit message (Expand)Author
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
2002-06-07extraction vers schemeletouzey
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-04-24petit bug dans les noms de fichiersletouzey
2002-04-08babioles de renommagesletouzey
2002-04-08ajout du mange-tout d'argument en ocaml + error en Haskell pour la constante ...letouzey
2002-03-26Refonte complete de la génération des types MLletouzey
2002-03-19remplacement des deux constants prop/arity par une seule dummy + pretty-print...letouzey
2002-03-05cas des constructeurs singletons. Messages d'erreur. Revision de test_extract...letouzey
2002-03-04Big commit extraction:letouzey
2002-02-15suite et fin (?) de haskell: gestion des modules, mise en place du'un testletouzey
2002-02-14qq inline manuels (sigS_rec ...) + utilisation de library_partletouzey
2002-02-12Test & correction de la production de code Haskellletouzey
2001-12-13compat ocaml 3.03filliatr
2001-12-10correction de bugs concernant la gestion des modules. debranchement du test d...letouzey
2001-11-29nouvel algo de conversion plus uniformebarras
2001-11-20hack temporaire concernant les remarks/modulesletouzey
2001-11-14Revolution culturelle: suppression des arguments propletouzey
2001-11-12suite du petit oupsletouzey
2001-11-12petit oupsletouzey
2001-11-12Refonte de extraction.ml. Traitement dans mlutil.ml des Empty Inductive (Texn)letouzey
2001-11-08Deplacement de l'optim singleton depuis extraction vers mlutil. Autres modifs...letouzey
2001-11-05optim: Idset au lieu de listletouzey
2001-11-05GROS COMMIT:barras
2001-11-03Creation de Recursive Extarction Moduleletouzey
2001-10-30legeres modifs pretty-print de l'extractionsletouzey
2001-10-26Fin de mise en place de l'option Optimize. Reorganisation du pretty-print. ET...letouzey
2001-10-23suite du seismeletouzey
2001-10-22chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les o...letouzey
2001-10-17Abstraction de l'immplementation de dirpath et implementation dans l'autre se...herbelin
2001-10-12Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...herbelin
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-09-19Changements de Extraction truc et Recursive Extractionletouzey
2001-09-18travail sur le Extract Constantletouzey
2001-08-10Parsingherbelin