aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction
AgeCommit message (Expand)Author
2006-12-17reparation bug 1239letouzey
2006-10-28Extension du polymorphisme de sorte au cas des définitions dans Type.herbelin
2006-10-04Correction bug #1211notin
2006-07-07Correction bug 1172 + correction en passant de la taille des paramètres de f...herbelin
2006-06-09oups: il faut penser a fermer la porte en partant (d'un fixpoint)letouzey
2006-06-09changements de dernieres minutes pour la 8.1 beta: letouzey
2006-06-08reparation bug 1006letouzey
2006-06-02debut de reparation du test d'extractionletouzey
2006-06-01reparation bug #1128letouzey
2006-05-23Nouvelle implantation du polymorphisme de sorte pour les familles inductivesherbelin
2006-04-28Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...notin
2006-04-27Standardisation nom option_app en option_mapherbelin
2006-04-20decoration des Tdummy pour pouvoir tuer tous les args de types (cf MapAVL.empty)letouzey
2005-12-28Remplacement Pp.qs par Pptactic.qsnewherbelin
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...herbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...herbelin
2005-12-21Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tact...herbelin
2005-12-16amelioration de l'extraction haskell: affichage du type des fonctions, et sup...letouzey
2005-12-16multiples ameliorations de l'extraction scheme:letouzey
2005-12-02Changement des named_contextgregoire
2005-12-01amelioration de la generation des unsafeCoerceletouzey
2005-11-30evite certaines eta-expansions cavalieresletouzey
2005-11-29correctif pour que type t = M.t contienne bien son M.letouzey
2005-11-17merci les warnings de 3.09 ...letouzey
2005-11-02Types inductifs parametriquesmohring
2005-08-19Sur le conseil de X.Leroy: x=[||] devient Array.length x=0letouzey
2005-02-18Standardisation of function names about global references (especially, renami...herbelin
2005-01-03HUGE COMMITsacerdot
2004-12-09travail sur les types extraitsletouzey
2004-11-18When a reference to a constructor is met its inductive type must be closed.sacerdot
2004-11-16Names.substitution (and related functions) and Term.subst_mps moved tosacerdot
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
2004-10-04un paquet de corrections de bugsletouzey
2004-09-06reparation des Extract Constant avec Haskellletouzey
2004-07-16Nouvelle en-têteherbelin
2004-07-14ajout des unsafeCoerce + 2 bugs haskellletouzey
2004-06-28Modules et Records: gros changements pour prendre en compte le nouveau mind_r...letouzey
2004-06-25correspondance des records et noms de champs de records entre un module et sa...letouzey
2004-04-05correction rapide du bug PR\#592letouzey
2004-03-25me = andouilleletouzey
2004-03-25Selon les optims, le let-in peut avoir maintenant des argsletouzey
2004-03-24nouvelle commande Set Extraction Flag: reglage fins des optimsletouzey
2004-03-23meme correction de bug, en moins bourrinletouzey
2004-03-22PolyList -> Listletouzey
2004-03-22correction d'un bug faisant inliner minus, mult, ...letouzey
2004-03-20petit rajeunissement du test d'extractionletouzey
2004-03-13Mise en place temporaire d'un afficheur de 'language' pour le traducteurherbelin
2004-02-13petit bug avec Extraction Optimizeletouzey
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...herbelin
2003-11-12les modifs depuis la 7.4letouzey