aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction
Commit message (Expand)AuthorAge
* 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
* merci les warnings de 3.09 ...Gravatar letouzey2005-11-17
* Types inductifs parametriquesGravatar mohring2005-11-02
* Sur le conseil de X.Leroy: x=[||] devient Array.length x=0Gravatar letouzey2005-08-19
* Standardisation of function names about global references (especially, renami...Gravatar herbelin2005-02-18
* HUGE COMMITGravatar sacerdot2005-01-03
* travail sur les types extraitsGravatar letouzey2004-12-09
* When a reference to a constructor is met its inductive type must be closed.Gravatar sacerdot2004-11-18
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* un paquet de corrections de bugsGravatar letouzey2004-10-04
* reparation des Extract Constant avec HaskellGravatar letouzey2004-09-06
* Nouvelle en-têteGravatar herbelin2004-07-16
* ajout des unsafeCoerce + 2 bugs haskellGravatar letouzey2004-07-14
* Modules et Records: gros changements pour prendre en compte le nouveau mind_r...Gravatar letouzey2004-06-28
* correspondance des records et noms de champs de records entre un module et sa...Gravatar letouzey2004-06-25
* correction rapide du bug PR\#592Gravatar letouzey2004-04-05
* me = andouilleGravatar letouzey2004-03-25
* Selon les optims, le let-in peut avoir maintenant des argsGravatar letouzey2004-03-25
* nouvelle commande Set Extraction Flag: reglage fins des optimsGravatar letouzey2004-03-24
* meme correction de bug, en moins bourrinGravatar letouzey2004-03-23
* PolyList -> ListGravatar letouzey2004-03-22
* correction d'un bug faisant inliner minus, mult, ...Gravatar letouzey2004-03-22
* petit rajeunissement du test d'extractionGravatar letouzey2004-03-20
* Mise en place temporaire d'un afficheur de 'language' pour le traducteurGravatar herbelin2004-03-13
* petit bug avec Extraction OptimizeGravatar letouzey2004-02-13
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* les modifs depuis la 7.4Gravatar letouzey2003-11-12
* TODOGravatar letouzey2003-11-12
* Extraction Module M devient simplement Extraction MGravatar letouzey2003-11-12