aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction
Commit message (Expand)AuthorAge
* nettoyage de code obsolete.Gravatar soubiran2008-03-14
* Ajout des alias de module dans le noyau.Gravatar soubiran2008-03-14
* Attempt of fix for extraction of modules typesGravatar letouzey2008-03-05
* dead codeGravatar letouzey2008-02-27
* typoGravatar letouzey2008-02-27
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
* Récupération d'une exception Not_foundGravatar notin2008-01-22
* cosmetics: after an extract inductive to bool, let's use if then elseGravatar letouzey2008-01-20
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Extraction inlines Wf.Fix by default (wish of Y.Bertot)Gravatar letouzey2007-11-21
* small fix of commit 10188: a string given via Extract Inductive can be emptyGravatar letouzey2007-10-25
* An error message instead of an empty extraction when the monolithic Gravatar letouzey2007-10-21
* Avoid the auto-inlining of small fixpoints like List.map.Gravatar letouzey2007-10-21
* Repair Haskell/Scheme extraction in the new extraction backend design: Gravatar letouzey2007-10-17
* Major reorganisation of the extraction "backend".Gravatar letouzey2007-10-17
* Extraction now checks that the required libraries are indeed loaded (bug #1144)Gravatar letouzey2007-10-09
* forbid extraction under a module typeGravatar letouzey2007-10-09
* Extract Inline/Inductive/Constant can now be used from inside a moduleGravatar letouzey2007-10-09
* Better use of tables for storing results of extract_ind (bug #1709)Gravatar letouzey2007-10-08
* Allowing infix constructors/types in a Extract InductiveGravatar letouzey2007-10-06
* Extraction: factorisation of identical branches in a matchGravatar letouzey2007-10-06
* Deletion of contrib/extraction/testGravatar letouzey2007-07-12
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* Suite au mail de Lionel a propos du Makefile: Gravatar letouzey2007-01-12
* un saut de ligne ...Gravatar letouzey2007-01-12
* suite de la reparation du bug 1239: apres les inds, les records et vars de typesGravatar letouzey2007-01-05
* reparation bug 1239Gravatar letouzey2006-12-17
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* Correction bug #1211Gravatar notin2006-10-04
* Correction bug 1172 + correction en passant de la taille des paramètres de f...Gravatar herbelin2006-07-07
* oups: il faut penser a fermer la porte en partant (d'un fixpoint)Gravatar letouzey2006-06-09
* changements de dernieres minutes pour la 8.1 beta: Gravatar letouzey2006-06-09
* reparation bug 1006Gravatar letouzey2006-06-08
* debut de reparation du test d'extractionGravatar letouzey2006-06-02
* reparation bug #1128Gravatar letouzey2006-06-01
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...Gravatar notin2006-04-28
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* decoration des Tdummy pour pouvoir tuer tous les args de types (cf MapAVL.empty)Gravatar letouzey2006-04-20
* Remplacement Pp.qs par Pptactic.qsnewGravatar herbelin2005-12-28
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...Gravatar herbelin2005-12-26
* Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tact...Gravatar herbelin2005-12-21
* amelioration de l'extraction haskell: affichage du type des fonctions, et sup...Gravatar letouzey2005-12-16
* multiples ameliorations de l'extraction scheme:Gravatar letouzey2005-12-16
* Changement des named_contextGravatar gregoire2005-12-02
* amelioration de la generation des unsafeCoerceGravatar letouzey2005-12-01
* evite certaines eta-expansions cavalieresGravatar letouzey2005-11-30
* correctif pour que type t = M.t contienne bien son M.Gravatar letouzey2005-11-29