aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Expand)Author
2002-03-21modification de l'auto-inliningletouzey
2002-03-20renversement du renommage des variablesletouzey
2002-03-20reparation du controle de l'apparition des termesletouzey
2002-03-20reorganisation des simplifications: letin eta-expansé apres le kill-dummyletouzey
2002-03-20un peu moins d'eta-expansion autour des Globletouzey
2002-03-19bug optimize_fix fait trop totletouzey
2002-03-19suite bug Dglob constantletouzey
2002-03-19bug avec les MLglob vraiment constantsletouzey
2002-03-19travail sur les stratégies de réductionletouzey
2002-03-19remplacement des deux constants prop/arity par une seule dummy + pretty-print...letouzey
2002-03-19Fix d'un bug sur le test des inversesdelahaye
2002-03-17Meilleure gestion de la reduction dans Fielddelahaye
2002-03-15epsilonletouzey
2002-03-15un peu de mise a jour de la doc extractionletouzey
2002-03-15evite les clash avec le type ocaml unitletouzey
2002-03-15gros commit: principalement ajout des lambdas arity + leur optimisation en te...letouzey
2002-03-14reparation semi setoid ringclrenard
2002-03-11Factorisation de la grammaire pour Extraction Language.letouzey
2002-03-05cas des constructeurs singletons. Messages d'erreur. Revision de test_extract...letouzey
2002-03-04Big commit extraction:letouzey
2002-03-04Nouveau Rewrite-in plus economiquebarras
2002-03-01Prise en compte des corps de letin dans les hypothèsesherbelin
2002-03-01convert_hyp a change de typebarras
2002-02-28Uniformisation convert_hypherbelin
2002-02-27modifs des preambules d'extraction modulaireletouzey
2002-02-25pretty print des Cases devenant des let-inletouzey
2002-02-21code mort dans tactinterp; plus de Debug On/Off dans Correctnessfilliatr
2002-02-20Changé le nom du module Errors (errors.mli, errors.ml) en Cerrors parceddr
2002-02-15petits changements cosmetiques sur les tactiquesbarras
2002-02-15suite et fin (?) de haskell: gestion des modules, mise en place du'un testletouzey
2002-02-15debut de gestion des open pour extraction modulaireletouzey
2002-02-14qq inline manuels (sigS_rec ...) + utilisation de library_partletouzey
2002-02-14- Reforme de la gestion des args recursifs (via arbres reguliers)barras
2002-02-12suppression de la condition de la permutation case/funletouzey
2002-02-12pretty printletouzey
2002-02-12Test & correction de la production de code Haskellletouzey
2002-02-08affichages avec prterm_env et non prterm; deb_print pour vraiment ne rien fai...filliatr
2002-02-07petit nettoyage de kernel/inductivebarras
2002-02-07un assert false de trop (MLexn peut avoir des args)letouzey
2002-02-06oubliletouzey
2002-02-06gros changement dans mlutil.ml: ajout d'une elimination globale des propletouzey
2002-02-05Ajout d'optimisations locales kill_propletouzey
2002-01-31adaptation de l'extraction aux changements de Christine concernant rec/rect e...letouzey
2002-01-31extraction des CoInductives via les Lazy d'ocamlletouzey
2002-01-25patch Omega (bug 129)filliatr
2002-01-23In Pcoq, the search commands had an erroneous behavior. Bound variablesbertot
2002-01-21Correction de Pierre Crégut pour le bug MERGE_EQherbelin
2002-01-21Zinv -> Zoppfilliatr
2002-01-18Bug MERGE_EQherbelin
2002-01-18Plusieurs arguments autorisés pour Require et Read Moduleherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 17:23:27 +0000