index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
/
extraction
/
mlutil.mli
Commit message (
Expand
)
Author
Age
*
nouvelle commande Set Extraction Flag: reglage fins des optims
letouzey
2004-03-24
*
BIG MAJ Extraction:
letouzey
2003-04-16
*
bugs/améliorations trouvés via FTA
letouzey
2003-02-21
*
Extraction des modules, enfin !
letouzey
2003-01-22
*
reorganisation des recherches de ref dans ml_decl
letouzey
2002-12-05
*
code cleanup (+ debut de commencement de modules)
letouzey
2002-12-05
*
nettoyage et reorganisation
letouzey
2002-11-04
*
L'extraction c'est magic cvs -n up
letouzey
2002-10-31
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Gros Remaniement Extraction:
letouzey
2002-07-16
*
ajout du mange-tout d'argument en ocaml + error en Haskell pour la constante ...
letouzey
2002-04-08
*
Refonte complete de la génération des types ML
letouzey
2002-03-26
*
remplacement des deux constants prop/arity par une seule dummy + pretty-print...
letouzey
2002-03-19
*
gros commit: principalement ajout des lambdas arity + leur optimisation en te...
letouzey
2002-03-15
*
Big commit extraction:
letouzey
2002-03-04
*
suite et fin (?) de haskell: gestion des modules, mise en place du'un test
letouzey
2002-02-15
*
Test & correction de la production de code Haskell
letouzey
2002-02-12
*
oubli
letouzey
2002-02-06
*
gros changement dans mlutil.ml: ajout d'une elimination globale des prop
letouzey
2002-02-06
*
Deplacement de l'optim singleton depuis extraction vers mlutil. Autres modifs...
letouzey
2001-11-08
*
Refonte du fichier mlutil.ml. Correction d'un bug d'optim case
letouzey
2001-11-07
*
GROS COMMIT:
barras
2001-11-05
*
suite des modifs concernant les optimisations divers
letouzey
2001-11-02
*
multiples bricoles. Cf mon TODO papier
letouzey
2001-10-31
*
Fin de mise en place de l'option Optimize. Reorganisation du pretty-print. ET...
letouzey
2001-10-26
*
chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les o...
letouzey
2001-10-22
*
Verification supplementaire avant optimisation singleton
letouzey
2001-09-19
*
travail sur le Extract Constant
letouzey
2001-09-18
*
mise en place extraction haskell
filliatr
2001-05-14
*
commentaires mlutil + binders_fold en cours
letouzey
2001-04-30
*
divers
filliatr
2001-04-23
*
Uncurryfy_ast inutile depuis l'eta-expansion dans extraction.ml.
letouzey
2001-04-23
*
optimizations extraction
filliatr
2001-04-20
*
deplacement de l'optimisation inductif singleton
letouzey
2001-04-19
*
eliminiation des singletons du genre sig + divers
letouzey
2001-04-13
*
nouvelle gestion des variables de type ML
letouzey
2001-04-12
*
réparation Correctness; options Extraction (changement de syntaxe)
filliatr
2001-04-10
*
branchement extraction en standard (pas de Require)
filliatr
2001-04-09
*
axiomes dans les types
filliatr
2001-04-04
*
rollback sur les commandes Extract Constant/Inductive; nettoyage et documenta...
filliatr
2001-04-04
*
commandes Extract Constant/Inductive; message d'erreur pour les axiomes
filliatr
2001-04-03
*
underscores pour les variables représentant des propositions
filliatr
2001-04-02
*
beta-reduction
filliatr
2001-03-30
*
conservation des arguments dans Prop (snif)
filliatr
2001-03-27
*
eta-expansion des constructeurs si necessaire (a posteriori en miniML)
filliatr
2001-03-23
*
mlutil
filliatr
2001-03-20