aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction
AgeCommit message (Expand)Author
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
2003-11-12TODOletouzey
2003-11-12Extraction Module M devient simplement Extraction Mletouzey
2003-11-10le pb du <<.v vu comme module>> engendre maintenant une erreurletouzey
2003-11-10message informant de l'ecriture d'un fichier extraitletouzey
2003-11-10révision du traitement des axiomes non réalisésletouzey
2003-11-10essai d'extraction sous un moduleletouzey
2003-11-09factorisation de (recursive) libraryletouzey
2003-10-10changement nouvelle syntaxe (pt fixes)barras
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
2003-10-06pour ocamlwebletouzey
2003-10-03Cacher les .v8herbelin
2003-09-22traducteur: affiche les commentaires a l'interieur des commandesbarras
2003-09-05bug dans calcul nb d'occurrencesletouzey
2003-08-28correction d'un stack overflow possible (PR#320)letouzey
2003-08-14Traduction mlnamesherbelin
2003-07-10bug typage du cases/identity: optim off si inductif avec varsletouzey
2003-07-10renommage des modules 1er niveau en monolithiqueletouzey
2003-07-08 bug match matchletouzey
2003-06-12enieme correction du nommage modulaireletouzey
2003-06-12fin de l'affichage des signatures de modules dans les *.mlletouzey
2003-06-08interaction entre fun/case permut et assert falseletouzey
2003-05-30oupsletouzey
2003-05-29:= dans un record engendre un LetIn qui n'etait pas géréletouzey
2003-05-28gestion plus fine des beta-redex lineaires (cf nb_occur_match)letouzey
2003-04-28bug concernant les projecteurs de Record avec args logiquesletouzey
2003-04-28adaptation a Acc_iterletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-05 10:23:08 +0000