aboutsummaryrefslogtreecommitdiff
path: root/kernel/closure.ml
AgeCommit message (Expand)Author
2012-11-28Kernel/closure: add eta red_kindpboutill
2012-11-22Monomorphization (kernel)ppedrot
2012-11-13More monomorphizationsppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-10-29Removed many calls to OCaml generic equality. This was done byppedrot
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
2012-03-02Noise for nothingpboutill
2011-08-08Esubst: make types of substitutions & lifts privatepuech
2011-02-17- Use transparency information all the way through unification andmsozeau
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-09-20Added eta-expansion in kernel, type inference and tactic unification,herbelin
2010-07-28ported r13340 to trunkbarras
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-05-09Added a few informations about file lineages (for the most part in kernel)herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-04-08Some dead code removal + cleanupsletouzey
2009-02-06pushed evar reduction in kernelbarras
2008-04-20Add the ability to give a transparent_state for conversion, tomsozeau
2008-03-10fold travaille maintenant sur la forme beta-iota-zeta réduite duherbelin
2007-07-12normalisation (by closure) was not performed under fixpointsbarras
2006-10-05Correction de deux cas où les types inductifs n'étaient pas comparésherbelin
2006-05-10correction bugs dans Cbv (beta n-aire)barras
2006-05-09subst. explicites avec vecteursbarras
2006-05-05amelioration de la machine interpretee (vecteurs au lieu de listes d'arguments)barras
2006-05-03bug #1096: whd_stack on one arg of conversion had side-effect on the other argbarras
2005-12-02Changement des named_contextgregoire
2005-11-18petites corrections + contournement bug projectionsbarras
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par o...herbelin
2005-08-22argument inutilisé de zip: toujours l'identitéletouzey
2005-07-13reactivation de l optim des fermeturesbarras
2005-07-13backtrack modif de knh...barras
2005-07-12test du tag de reductionbarras
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-07-16Nouvelle en-têteherbelin
2003-08-06Ajout de l'opti des fermeture (mais debranche pour l'instant)barras
2003-08-05Improved reduction machine with closure: should use less memorybarras
2003-04-16simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...letouzey
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-10-15pattern-matching avec cas inutilise dans closurebarras
2002-08-16Strengthenning rules for modules + No modules in sectionscoq
2002-08-02Modules dans COQ\!\!\!\!coq
2002-03-12open Univ inutilecourant
2002-01-30cosmetiqueherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:14:41 +0000