aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction/extraction.ml
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-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-05-23Nouvelle implantation du polymorphisme de sorte pour les familles inductivesherbelin
2006-04-20decoration des Tdummy pour pouvoir tuer tous les args de types (cf MapAVL.empty)letouzey
2005-12-02Changement des named_contextgregoire
2005-11-30evite certaines eta-expansions cavalieresletouzey
2005-11-17merci les warnings de 3.09 ...letouzey
2005-11-02Types inductifs parametriquesmohring
2005-02-18Standardisation of function names about global references (especially, renami...herbelin
2004-12-09travail sur les types extraitsletouzey
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
2004-07-16Nouvelle en-têteherbelin
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
2003-11-10révision du traitement des axiomes non réalisésletouzey
2003-09-22traducteur: affiche les commentaires a l'interieur des commandesbarras
2003-08-28correction d'un stack overflow possible (PR#320)letouzey
2003-05-29:= dans un record engendre un LetIn qui n'etait pas géréletouzey
2003-04-28bug concernant les projecteurs de Record avec args logiquesletouzey
2003-04-16BIG MAJ Extraction:letouzey
2003-03-25Extract Constant marche avec les axiomes schémas de typesletouzey
2003-03-11pour ocamlwebletouzey
2003-02-21bugs/améliorations trouvés via FTAletouzey
2003-02-03encore un long_knletouzey
2003-02-02plus d'environment fixe cur_env mais un environment evolutifletouzey
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-28nouvelle gestion des constantes de typeletouzey
2003-01-23oubli des add_recursors singleton logiquesletouzey
2003-01-22Extraction des modules, enfin !letouzey
2002-12-19les empty ind et les singletons etaient oublies par add_recursorsletouzey
2002-12-13une branche de case inutileletouzey
2002-12-09petit bugletouzey
2002-12-09chamboulement du codage des indcutifs extraits; deplacements des tables; ...letouzey
2002-12-05code cleanup (+ debut de commencement de modules)letouzey
2002-11-28 bug pp letin + un inductif constant n'est pas un recordletouzey
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-04nettoyage et reorganisationletouzey
2002-10-31L'extraction c'est magic cvs -n upletouzey
2002-10-07Lazy manuelles dans le codecoq
2002-10-05Lazy experimentale temporaire...coq
2002-08-02Modules dans COQ\!\!\!\!coq
2002-07-24reparation d'un bug (dummy_lams -> anonym_lams) + chgmt structutr d'un ml_typeletouzey
2002-07-17reparation temporaire(?) a coup de MLdummy'letouzey