aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction
AgeCommit message (Expand)Author
2003-03-25Extract Constant marche avec les axiomes schémas de typesletouzey
2003-03-11pour coq-ideletouzey
2003-03-11pour ocamlwebletouzey
2003-02-21bugs/améliorations trouvés via FTAletouzey
2003-02-03maj status de l'extraction des modulesletouzey
2003-02-03hack horrible pour renommage dans Modules Types et Functeursletouzey
2003-02-03encore un long_knletouzey
2003-02-02plus d'environment fixe cur_env mais un environment evolutifletouzey
2003-01-30fignolageletouzey
2003-01-30pb d'hier resolu. Recommitletouzey
2003-01-29apres le backtrack precedent, remise de trois points precis et sursletouzey
2003-01-29Ca a tout pété -> Bactrack a la version d'hierletouzey
2003-01-29affichage module et module typeletouzey
2003-01-29affichage module et module typeletouzey
2003-01-29affichage module et module typeletouzey
2003-01-28workaround en attendant traitement reel des modules typesletouzey
2003-01-28amelioration du pretty-print des modulesletouzey
2003-01-28nouvelle gestion des constantes de typeletouzey
2003-01-23oubli des add_recursors singleton logiquesletouzey
2003-01-23maj V7.4letouzey
2003-01-22petit bug pp haskellletouzey
2003-01-22Extraction des modules, enfin !letouzey
2003-01-09Export M + Module M <: SIGcoq
2002-12-19suppression de l'archive cvs d'un bout de debugletouzey
2002-12-19les empty ind et les singletons etaient oublies par add_recursorsletouzey
2002-12-18stupide inlining des construsteursletouzey
2002-12-13debut de parcours des modulesletouzey
2002-12-13une branche de case inutileletouzey
2002-12-09ppletouzey
2002-12-09petit bugletouzey
2002-12-09chamboulement du codage des indcutifs extraits; deplacements des tables; ...letouzey
2002-12-05reorganisation des recherches de ref dans ml_declletouzey
2002-12-05code cleanup (+ debut de commencement de modules)letouzey
2002-12-03la table PARAMETER n'existe plus (mergé dans la table CONSTANT)letouzey
2002-11-292 bugs: 1) projections pas renommées 2) mutual fixpoints a l'enversletouzey
2002-11-29cosmetiqueletouzey
2002-11-28Remaniement du pp, suite: vers un renommage modulaire correcteletouzey
2002-11-28suite et fin des records avec ocamlletouzey
2002-11-28 bug pp letin + un inductif constant n'est pas un recordletouzey
2002-11-28Re-Oupsletouzey
2002-11-28Oupsletouzey
2002-11-28Reorganisation du pretty-print:letouzey
2002-11-27Extraction des Record, suiteletouzey
2002-11-26debut de support des records camlletouzey
2002-11-25correction bug n°191letouzey
2002-11-25cleanup table.ml + erreur si Extraction Inline sous sectionletouzey
2002-11-18remaniement de test_extraction.vletouzey
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-11-05cosmetiqueletouzey
2002-11-04un bug concernant l'expansion des Map_rec si Map n'est pas ouvertletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 13:13:26 +0000