aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction
Commit message (Expand)AuthorAge
* Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...Gravatar herbelin2001-10-12
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* correction de deux petits bugs: case_identité trop fort et Anomaly dans le t...Gravatar letouzey2001-10-01
* correction du eta_expanseGravatar letouzey2001-09-20
* bug affichage des termes ml fournisGravatar letouzey2001-09-20
* utilisation du nouveau get_sort_family_ofGravatar letouzey2001-09-20
* changements mineurs du testGravatar letouzey2001-09-20
* ajout du fichier CHANGESGravatar letouzey2001-09-19
* adaptation a la nouvelle syntaxe Extract Inlined ConstantGravatar letouzey2001-09-19
* Changements de Extraction truc et Recursive ExtractionGravatar letouzey2001-09-19
* Deux nouvelles optimisations pour CasesGravatar letouzey2001-09-19
* Verification supplementaire avant optimisation singletonGravatar letouzey2001-09-19
* travail sur le Extract ConstantGravatar letouzey2001-09-18
* changement du make depend en vu du make realsGravatar letouzey2001-09-10
* bug de rename_global modulaire corrige'Gravatar letouzey2001-09-10
* ParsingGravatar herbelin2001-08-10
* Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...Gravatar herbelin2001-07-21
* Nettoyage/restructuration des ensembles d'indicateurs de réductionsGravatar herbelin2001-07-02
* 2 bugs: typevarlist pour inductifs + args pour flexiblesGravatar letouzey2001-06-22
* Oups: flingait les Dglob dans optimizeGravatar letouzey2001-05-25
* majGravatar letouzey2001-05-22
* suite du musée des horreursGravatar letouzey2001-05-22
* ordre des inductifs + axiome-typeGravatar letouzey2001-05-22
* mise en place extraction haskellGravatar filliatr2001-05-14
* bug castGravatar letouzey2001-05-11
* exemples MagicGravatar letouzey2001-05-10
* retouche de extract_inductive_declarationGravatar letouzey2001-05-10
* nettoyage extractionGravatar filliatr2001-05-09
* cleanup + comments, toujoursGravatar letouzey2001-05-09
* commentairesGravatar letouzey2001-05-04
* Changement de la structure des points fixesGravatar barras2001-05-03
* commentaires sur renommages des var dans extract_typeGravatar letouzey2001-05-02
* cleanup, commentsGravatar letouzey2001-04-30
* ocamlwebGravatar filliatr2001-04-30
* commentaires mlutil + binders_fold en coursGravatar letouzey2001-04-30
* make reals prend en compte tous les .vo de theories/RealsGravatar filliatr2001-04-25
* README avec ref (2)Gravatar letouzey2001-04-24
* TODO in v.o., test/Makefile moins pire, README avec refGravatar letouzey2001-04-24
* Ajout du .dependGravatar mohring2001-04-24
* Retire theories/NumGravatar mohring2001-04-24
* Correction typosGravatar mohring2001-04-24
* ajout d'un fichier READMEGravatar letouzey2001-04-24
* Fin d'optimisation (cas modules) + warning pour coind & ocamlGravatar letouzey2001-04-24
* cofix_warning dans les parametres d'extractionGravatar filliatr2001-04-24
* forme codeGravatar filliatr2001-04-23
* mise a jourGravatar letouzey2001-04-23
* realisation des realsGravatar letouzey2001-04-23
* Gros nain avec de Bruijn...Gravatar letouzey2001-04-23
* diversGravatar filliatr2001-04-23
* nettoyageGravatar filliatr2001-04-23