aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2014-03-04Fixing pervasives equalities in Vconv.Pierre-Marie Pédrot
2014-03-03Fixing Pervasives.equality in extraction.Pierre-Marie Pédrot
2014-03-03Fixing pervasive equalities. In particular, I removed the code that deletedPierre-Marie Pédrot
2014-03-03Removing generic hashes in kernel.Pierre-Marie Pédrot
2014-03-03Kernel names are implemented using records.Pierre-Marie Pédrot
2014-03-03Fixing generic hashes and replacing them with proper ones.Pierre-Marie Pédrot
2014-03-02Fixing generic Hashtbl.hash in Constr.Pierre-Marie Pédrot
2014-03-01Hunting pervasive equality in native compiler. It seems they were used forPierre-Marie Pédrot
2014-02-26STM: when batch compiling a vo, assert we behave conservativelyEnrico Tassi
2014-02-26Lazyconstr -> OpaqueproofEnrico Tassi
2014-02-26remoteCounter: backup/restoreEnrico Tassi
2014-02-26univ: removing dead codeEnrico Tassi
2014-02-26New compilation mode -vi2voEnrico Tassi
2014-02-20Optimization in kernel/vars.ml: directly allocate a fixed-size block in thePierre-Marie Pédrot
2014-02-11Made Pre_env.lazy_val opaque.Pierre-Marie Pédrot
2014-02-09Small optimizations in Closure:Pierre-Marie Pédrot
2014-02-03Tracking memory misallocation by trying to improve sharing.Pierre-Marie Pédrot
2014-02-03Allocation-friendly mapping functions in Nametab.Pierre-Marie Pédrot
2014-01-18Relaxing the sort elimination check to allow for let-bindings in arities.Maxime Dénès
2014-01-15Christmas is over...Maxime Dénès
2014-01-07STM: additional fix for STM + vm_computeEnrico Tassi
2014-01-06STM: fix worker crash when doing vm_computeEnrico Tassi
2014-01-05Proof_using: new syntax + suggestionEnrico Tassi
2014-01-05Environ: export API to transitively close a set of section variablesEnrico Tassi
2014-01-05Paral-ITP: cleanup of command line flags and more conservative defaultEnrico Tassi
2014-01-04.vi files: .vo files without proofsEnrico Tassi
2014-01-04kernel: save in aux the list of section variables usedEnrico Tassi
2014-01-04Remove obsolete comment about Let being processed synchronouslyEnrico Tassi
2013-12-30Support for evars and metas in native compiler.Maxime Dénès
2013-12-29Avoid generating .ml files in native compiler.Maxime Dénès
2013-12-29Got rid of unused lazy flag in the native compiler.Maxime Dénès
2013-12-28Revert "Partial revert of r16711"Maxime Dénès
2013-12-28Removing native_name reference from constant_body.Maxime Dénès
2013-12-24STM: capture type checking error (Closes: 3195)Enrico Tassi
2013-12-24Qed: feedback when type checking is doneEnrico Tassi
2013-12-17Tentative fix of the guardedness checker by Christine and me. All stdlib and ...Matthieu Sozeau
2013-12-16A few fixes to the build system (mostly for ocamlbuild)Pierre Letouzey
2013-12-15Do not overallocate closures' named environments in infos. Modifying the accessPierre-Marie Pédrot
2013-11-27Reduction: every n iterations a slaves process checks for interruptionEnrico Tassi
2013-11-24Slightly more efficient zip function in Closure.Pierre-Marie Pédrot
2013-11-23Small allocation improvement in Closure.Pierre-Marie Pédrot
2013-11-15Revert "Fast lookup_named in environments, based on maps instead of lists."ppedrot
2013-11-13Fast lookup_named in environments, based on maps instead of lists.ppedrot
2013-11-06Less partial applications in Vars, as well as better memory allocation.ppedrot
2013-11-04Using allocation-free version of Array higher-order function in criticalppedrot
2013-11-04Evar module now uses default Int maps and sets.ppedrot
2013-11-02Closure: fix an issue with r16959 spotted by Matthieuletouzey
2013-10-31Mod_subst.update_delta_resolver : avoid loosing Inline(_,Some _)letouzey
2013-10-31Fixing Kerpair.hash. Since the beginning, it dit not respect the typeppedrot
2013-10-31Future: better doc + restore ~pure optimizationgareuselesinge
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:59:51 +0000