aboutsummaryrefslogtreecommitdiff
path: root/kernel/closure.ml
AgeCommit message (Expand)Author
2013-11-04Using allocation-free version of Array higher-order function in criticalppedrot
2013-11-02Closure: fix an issue with r16959 spotted by Matthieuletouzey
2013-10-31Conv_orable made functional and part of pre_envgareuselesinge
2013-10-31Avoiding useless allocations in Closure.ppedrot
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-24Specializing hash functions for widely used types.ppedrot
2013-10-24Turn many List.assoc into List.assoc_fletouzey
2013-10-23cList.index is now cList.index_f, same for index0letouzey
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-18Modulification of nameppedrot
2012-12-14Modulification of identifierppedrot
2012-12-08Small optimization in Closure: replaced an index list with an array.ppedrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:56:59 +0000