aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction/mlutil.mli
Commit message (Expand)AuthorAge
* mise en place extraction haskellGravatar filliatr2001-05-14
* commentaires mlutil + binders_fold en coursGravatar letouzey2001-04-30
* diversGravatar filliatr2001-04-23
* Uncurryfy_ast inutile depuis l'eta-expansion dans extraction.ml.Gravatar letouzey2001-04-23
* optimizations extractionGravatar filliatr2001-04-20
* deplacement de l'optimisation inductif singletonGravatar letouzey2001-04-19
* eliminiation des singletons du genre sig + diversGravatar letouzey2001-04-13
* nouvelle gestion des variables de type MLGravatar letouzey2001-04-12
* réparation Correctness; options Extraction (changement de syntaxe)Gravatar filliatr2001-04-10
* branchement extraction en standard (pas de Require)Gravatar filliatr2001-04-09
* axiomes dans les typesGravatar filliatr2001-04-04
* rollback sur les commandes Extract Constant/Inductive; nettoyage et documenta...Gravatar filliatr2001-04-04
* commandes Extract Constant/Inductive; message d'erreur pour les axiomesGravatar filliatr2001-04-03
* underscores pour les variables représentant des propositionsGravatar filliatr2001-04-02
* beta-reductionGravatar filliatr2001-03-30
* conservation des arguments dans Prop (snif)Gravatar filliatr2001-03-27
* eta-expansion des constructeurs si necessaire (a posteriori en miniML)Gravatar filliatr2001-03-23
* mlutilGravatar filliatr2001-03-20