index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
contrib
/
extraction
/
haskell.ml
Age
Commit message (
Expand
)
Author
2009-03-20
Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...
letouzey
2008-11-06
Cosmetic: no more whitespace at end of lines in extraction files
letouzey
2008-11-05
Better extraction renaming phase (fix #1914 plus other non-reported bugs)
letouzey
2007-10-17
Repair Haskell/Scheme extraction in the new extraction backend design:
letouzey
2007-10-17
Major reorganisation of the extraction "backend".
letouzey
2007-10-06
Extraction: factorisation of identical branches in a match
letouzey
2006-06-09
changements de dernieres minutes pour la 8.1 beta:
letouzey
2006-04-20
decoration des Tdummy pour pouvoir tuer tous les args de types (cf MapAVL.empty)
letouzey
2005-12-16
amelioration de l'extraction haskell: affichage du type des fonctions, et sup...
letouzey
2005-12-01
amelioration de la generation des unsafeCoerce
letouzey
2005-08-19
Sur le conseil de X.Leroy: x=[||] devient Array.length x=0
letouzey
2004-10-04
un paquet de corrections de bugs
letouzey
2004-09-06
reparation des Extract Constant avec Haskell
letouzey
2004-07-16
Nouvelle en-tête
herbelin
2004-07-14
ajout des unsafeCoerce + 2 bugs haskell
letouzey
2004-06-28
Modules et Records: gros changements pour prendre en compte le nouveau mind_r...
letouzey
2004-03-25
Selon les optims, le let-in peut avoir maintenant des args
letouzey
2003-11-10
révision du traitement des axiomes non réalisés
letouzey
2003-04-16
BIG MAJ Extraction:
letouzey
2003-02-02
plus d'environment fixe cur_env mais un environment evolutif
letouzey
2003-01-22
petit bug pp haskell
letouzey
2003-01-22
Extraction des modules, enfin !
letouzey
2002-12-09
chamboulement du codage des indcutifs extraits; deplacements des tables; ...
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-11-28
bug pp letin + un inductif constant n'est pas un record
letouzey
2002-11-28
Reorganisation du pretty-print:
letouzey
2002-10-31
L'extraction c'est magic cvs -n up
letouzey
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-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-21
considerations de pretty-print
letouzey
2002-03-19
remplacement des deux constants prop/arity par une seule dummy + pretty-print...
letouzey
2002-03-15
gros commit: principalement ajout des lambdas arity + leur optimisation en te...
letouzey
2002-03-04
Big commit extraction:
letouzey
2002-02-27
modifs des preambules d'extraction modulaire
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
pretty print
letouzey
2002-02-12
Test & correction de la production de code Haskell
letouzey
2002-02-07
un assert false de trop (MLexn peut avoir des args)
letouzey
2002-02-06
gros changement dans mlutil.ml: ajout d'une elimination globale des prop
letouzey
2001-12-21
maj CHANGES extraction + bug extraction & _
letouzey
2001-12-18
typo de parenthèsage + suppression de string (= str maintenant)
letouzey
2001-12-13
compat ocaml 3.03
filliatr
2001-11-12
Refonte de extraction.ml. Traitement dans mlutil.ml des Empty Inductive (Texn)
letouzey
2001-11-05
GROS COMMIT:
barras
2001-11-03
Creation de Recursive Extarction Module
letouzey
2001-11-02
suite des modifs concernant les optimisations divers
letouzey
[next]