aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction/extract_env.ml
Commit message (Expand)AuthorAge
* BIG MAJ Extraction:Gravatar letouzey2003-04-16
* plus d'environment fixe cur_env mais un environment evolutifGravatar letouzey2003-02-02
* apres le backtrack precedent, remise de trois points precis et sursGravatar letouzey2003-01-29
* Ca a tout pété -> Bactrack a la version d'hierGravatar letouzey2003-01-29
* affichage module et module typeGravatar letouzey2003-01-29
* Extraction des modules, enfin !Gravatar letouzey2003-01-22
* Export M + Module M <: SIGGravatar coq2003-01-09
* debut de parcours des modulesGravatar letouzey2002-12-13
* chamboulement du codage des indcutifs extraits; deplacements des tables; ...Gravatar letouzey2002-12-09
* reorganisation des recherches de ref dans ml_declGravatar letouzey2002-12-05
* code cleanup (+ debut de commencement de modules)Gravatar letouzey2002-12-05
* Remaniement du pp, suite: vers un renommage modulaire correcteGravatar letouzey2002-11-28
* L'extraction c'est magic cvs -n upGravatar letouzey2002-10-31
* suite chgt liés aux modulesGravatar letouzey2002-09-24
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* reparation d'un bug (dummy_lams -> anonym_lams) + chgmt structutr d'un ml_typeGravatar letouzey2002-07-24
* Gros Remaniement Extraction:Gravatar letouzey2002-07-16
* extraction vers schemeGravatar letouzey2002-06-07
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* petit bug dans les noms de fichiersGravatar letouzey2002-04-24
* babioles de renommagesGravatar letouzey2002-04-08
* ajout du mange-tout d'argument en ocaml + error en Haskell pour la constante ...Gravatar letouzey2002-04-08
* Refonte complete de la génération des types MLGravatar letouzey2002-03-26
* remplacement des deux constants prop/arity par une seule dummy + pretty-print...Gravatar letouzey2002-03-19
* cas des constructeurs singletons. Messages d'erreur. Revision de test_extract...Gravatar letouzey2002-03-05
* Big commit extraction:Gravatar letouzey2002-03-04
* suite et fin (?) de haskell: gestion des modules, mise en place du'un testGravatar letouzey2002-02-15
* qq inline manuels (sigS_rec ...) + utilisation de library_partGravatar letouzey2002-02-14
* Test & correction de la production de code HaskellGravatar letouzey2002-02-12
* compat ocaml 3.03Gravatar filliatr2001-12-13
* correction de bugs concernant la gestion des modules. debranchement du test d...Gravatar letouzey2001-12-10
* nouvel algo de conversion plus uniformeGravatar barras2001-11-29
* hack temporaire concernant les remarks/modulesGravatar letouzey2001-11-20
* Revolution culturelle: suppression des arguments propGravatar letouzey2001-11-14
* suite du petit oupsGravatar letouzey2001-11-12
* petit oupsGravatar letouzey2001-11-12
* Refonte de extraction.ml. Traitement dans mlutil.ml des Empty Inductive (Texn)Gravatar letouzey2001-11-12
* Deplacement de l'optim singleton depuis extraction vers mlutil. Autres modifs...Gravatar letouzey2001-11-08
* optim: Idset au lieu de listGravatar letouzey2001-11-05
* GROS COMMIT:Gravatar barras2001-11-05
* Creation de Recursive Extarction ModuleGravatar letouzey2001-11-03
* legeres modifs pretty-print de l'extractionsGravatar letouzey2001-10-30
* Fin de mise en place de l'option Optimize. Reorganisation du pretty-print. ET...Gravatar letouzey2001-10-26
* suite du seismeGravatar letouzey2001-10-23
* chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les o...Gravatar letouzey2001-10-22
* Abstraction de l'immplementation de dirpath et implementation dans l'autre se...Gravatar herbelin2001-10-17
* Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...Gravatar herbelin2001-10-12
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* Changements de Extraction truc et Recursive ExtractionGravatar letouzey2001-09-19
* travail sur le Extract ConstantGravatar letouzey2001-09-18