aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction
Commit message (Expand)AuthorAge
* bug concernant les projecteurs de Record avec args logiquesGravatar letouzey2003-04-28
* adaptation a Acc_iterGravatar letouzey2003-04-28
* OoopsGravatar letouzey2003-04-17
* temporaireGravatar letouzey2003-04-17
* BIG MAJ Extraction:Gravatar letouzey2003-04-16
* Extract Constant marche avec les axiomes schémas de typesGravatar letouzey2003-03-25
* pour coq-ideGravatar letouzey2003-03-11
* pour ocamlwebGravatar letouzey2003-03-11
* bugs/améliorations trouvés via FTAGravatar letouzey2003-02-21
* maj status de l'extraction des modulesGravatar letouzey2003-02-03
* hack horrible pour renommage dans Modules Types et FuncteursGravatar letouzey2003-02-03
* encore un long_knGravatar letouzey2003-02-03
* plus d'environment fixe cur_env mais un environment evolutifGravatar letouzey2003-02-02
* fignolageGravatar letouzey2003-01-30
* pb d'hier resolu. RecommitGravatar letouzey2003-01-30
* apres le backtrack precedent, remise de trois points precis et sursGravatar letouzey2003-01-29
* Ca a tout pété -> Bactrack a la version d'hierGravatar letouzey2003-01-29
* affichage module et module typeGravatar letouzey2003-01-29
* affichage module et module typeGravatar letouzey2003-01-29
* affichage module et module typeGravatar letouzey2003-01-29
* workaround en attendant traitement reel des modules typesGravatar letouzey2003-01-28
* amelioration du pretty-print des modulesGravatar letouzey2003-01-28
* nouvelle gestion des constantes de typeGravatar letouzey2003-01-28
* oubli des add_recursors singleton logiquesGravatar letouzey2003-01-23
* maj V7.4Gravatar letouzey2003-01-23
* petit bug pp haskellGravatar letouzey2003-01-22
* Extraction des modules, enfin !Gravatar letouzey2003-01-22
* Export M + Module M <: SIGGravatar coq2003-01-09
* suppression de l'archive cvs d'un bout de debugGravatar letouzey2002-12-19
* les empty ind et les singletons etaient oublies par add_recursorsGravatar letouzey2002-12-19
* stupide inlining des construsteursGravatar letouzey2002-12-18
* debut de parcours des modulesGravatar letouzey2002-12-13
* une branche de case inutileGravatar letouzey2002-12-13
* ppGravatar letouzey2002-12-09
* petit bugGravatar letouzey2002-12-09
* chamboulement du codage des indcutifs extraits; deplacements des tables; ...Gravatar letouzey2002-12-09
* reorganisation des recherches de ref dans ml_declGravatar letouzey2002-12-05
* code cleanup (+ debut de commencement de modules)Gravatar letouzey2002-12-05
* la table PARAMETER n'existe plus (mergé dans la table CONSTANT)Gravatar letouzey2002-12-03
* 2 bugs: 1) projections pas renommées 2) mutual fixpoints a l'enversGravatar letouzey2002-11-29
* cosmetiqueGravatar letouzey2002-11-29
* Remaniement du pp, suite: vers un renommage modulaire correcteGravatar letouzey2002-11-28
* suite et fin des records avec ocamlGravatar letouzey2002-11-28
* bug pp letin + un inductif constant n'est pas un recordGravatar letouzey2002-11-28
* Re-OupsGravatar letouzey2002-11-28
* OupsGravatar letouzey2002-11-28
* Reorganisation du pretty-print:Gravatar letouzey2002-11-28
* Extraction des Record, suiteGravatar letouzey2002-11-27
* debut de support des records camlGravatar letouzey2002-11-26
* correction bug n°191Gravatar letouzey2002-11-25