index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
contrib
/
extraction
/
extract_env.ml
Age
Commit message (
Expand
)
Author
2003-02-02
plus d'environment fixe cur_env mais un environment evolutif
letouzey
2003-01-29
apres le backtrack precedent, remise de trois points precis et surs
letouzey
2003-01-29
Ca a tout pété -> Bactrack a la version d'hier
letouzey
2003-01-29
affichage module et module type
letouzey
2003-01-22
Extraction des modules, enfin !
letouzey
2003-01-09
Export M + Module M <: SIG
coq
2002-12-13
debut de parcours des modules
letouzey
2002-12-09
chamboulement du codage des indcutifs extraits; deplacements des tables; ...
letouzey
2002-12-05
reorganisation des recherches de ref dans ml_decl
letouzey
2002-12-05
code cleanup (+ debut de commencement de modules)
letouzey
2002-11-28
Remaniement du pp, suite: vers un renommage modulaire correcte
letouzey
2002-10-31
L'extraction c'est magic cvs -n up
letouzey
2002-09-24
suite chgt liés aux modules
letouzey
2002-08-02
Modules dans COQ\!\!\!\!
coq
2002-07-24
reparation d'un bug (dummy_lams -> anonym_lams) + chgmt structutr d'un ml_type
letouzey
2002-07-16
Gros Remaniement Extraction:
letouzey
2002-06-07
extraction vers scheme
letouzey
2002-05-29
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-04-24
petit bug dans les noms de fichiers
letouzey
2002-04-08
babioles de renommages
letouzey
2002-04-08
ajout du mange-tout d'argument en ocaml + error en Haskell pour la constante ...
letouzey
2002-03-26
Refonte complete de la génération des types ML
letouzey
2002-03-19
remplacement des deux constants prop/arity par une seule dummy + pretty-print...
letouzey
2002-03-05
cas des constructeurs singletons. Messages d'erreur. Revision de test_extract...
letouzey
2002-03-04
Big commit extraction:
letouzey
2002-02-15
suite et fin (?) de haskell: gestion des modules, mise en place du'un test
letouzey
2002-02-14
qq inline manuels (sigS_rec ...) + utilisation de library_part
letouzey
2002-02-12
Test & correction de la production de code Haskell
letouzey
2001-12-13
compat ocaml 3.03
filliatr
2001-12-10
correction de bugs concernant la gestion des modules. debranchement du test d...
letouzey
2001-11-29
nouvel algo de conversion plus uniforme
barras
2001-11-20
hack temporaire concernant les remarks/modules
letouzey
2001-11-14
Revolution culturelle: suppression des arguments prop
letouzey
2001-11-12
suite du petit oups
letouzey
2001-11-12
petit oups
letouzey
2001-11-12
Refonte de extraction.ml. Traitement dans mlutil.ml des Empty Inductive (Texn)
letouzey
2001-11-08
Deplacement de l'optim singleton depuis extraction vers mlutil. Autres modifs...
letouzey
2001-11-05
optim: Idset au lieu de list
letouzey
2001-11-05
GROS COMMIT:
barras
2001-11-03
Creation de Recursive Extarction Module
letouzey
2001-10-30
legeres modifs pretty-print de l'extractions
letouzey
2001-10-26
Fin de mise en place de l'option Optimize. Reorganisation du pretty-print. ET...
letouzey
2001-10-23
suite du seisme
letouzey
2001-10-22
chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les o...
letouzey
2001-10-17
Abstraction de l'immplementation de dirpath et implementation dans l'autre se...
herbelin
2001-10-12
Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...
herbelin
2001-10-09
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-09-19
Changements de Extraction truc et Recursive Extraction
letouzey
2001-09-18
travail sur le Extract Constant
letouzey
2001-08-10
Parsing
herbelin
[next]