aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Reduction: every n iterations a slaves process checks for interruptionGravatar Enrico Tassi2013-11-27
* Slightly more efficient zip function in Closure.Gravatar Pierre-Marie Pédrot2013-11-24
* Small allocation improvement in Closure.Gravatar Pierre-Marie Pédrot2013-11-23
* Revert "Fast lookup_named in environments, based on maps instead of lists."Gravatar ppedrot2013-11-15
* Fast lookup_named in environments, based on maps instead of lists.Gravatar ppedrot2013-11-13
* Less partial applications in Vars, as well as better memory allocation.Gravatar ppedrot2013-11-06
* Using allocation-free version of Array higher-order function in criticalGravatar ppedrot2013-11-04
* Evar module now uses default Int maps and sets.Gravatar ppedrot2013-11-04
* Closure: fix an issue with r16959 spotted by MatthieuGravatar letouzey2013-11-02
* Mod_subst.update_delta_resolver : avoid loosing Inline(_,Some _)Gravatar letouzey2013-10-31
* Fixing Kerpair.hash. Since the beginning, it dit not respect the typeGravatar ppedrot2013-10-31
* Future: better doc + restore ~pure optimizationGravatar gareuselesinge2013-10-31
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
* Avoiding useless allocations in Closure.Gravatar ppedrot2013-10-31
* Do not generate useless argument arrays in whd_* functions.Gravatar ppedrot2013-10-29
* Allocation-friendly version of [Pre_env.push_named].Gravatar ppedrot2013-10-29
* Optimizing universes: tail-rec, allocation friendly [compare_leq].Gravatar ppedrot2013-10-29
* Native compiler: library compilation errors are now non fatal.Gravatar mdenes2013-10-28
* More sharing in Constr.map_with_binders.Gravatar ppedrot2013-10-27
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* inductive.ml : get rid of some obvious (Lazy.force (lazy t))Gravatar letouzey2013-10-24
* Rtree : cleanup of the comparing codeGravatar letouzey2013-10-24
* Specializing hash functions for widely used types.Gravatar ppedrot2013-10-24
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* cList: a few alternative to hashtbl-based uniquize, distinct, subsetGravatar letouzey2013-10-23
* cList.index is now cList.index_f, same for index0Gravatar letouzey2013-10-23
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
* Optimizing Vars.replace_varsGravatar ppedrot2013-10-23
* Removing some generic equalities.Gravatar ppedrot2013-10-22
* Various optimizations in Constr, such as term sharing and allocationGravatar ppedrot2013-10-22
* Future: ported to Ephemeron + exception enhancingGravatar gareuselesinge2013-10-18
* Fix comment for new string syntax (OCaml trunk).Gravatar xclerc2013-10-04
* A shallow copy of a pre_env does not contain the vm cacheGravatar gareuselesinge2013-10-03
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* Slightly more compact representation of 'a substituted type,Gravatar ppedrot2013-09-14
* ind_tables: properly handling side effectsGravatar gareuselesinge2013-08-30
* Remove Obj.magic from safe typingGravatar gareuselesinge2013-08-30
* Added a more efficient way to recover the domain of a map.Gravatar ppedrot2013-08-25
* Replacing lists by sets in clear tactic.Gravatar ppedrot2013-08-25
* Fix computation of discharged hyps for inductive types forgetting the conclus...Gravatar msozeau2013-08-23
* Misc changes around coqtop.ml :Gravatar letouzey2013-08-22
* More complete hashcons : lists (dirpath), arrays (constr)Gravatar letouzey2013-08-22
* Partial revert of r16711Gravatar letouzey2013-08-20
* Universe counters on slaves are in sync with masterGravatar gareuselesinge2013-08-20
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* Declareops + Modops : more clever substitutionsGravatar letouzey2013-08-20
* Mod_typing : code cleanupGravatar letouzey2013-08-20
* Safe_typing code refactoringGravatar letouzey2013-08-20