aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Using HMaps in global references.Gravatar Pierre-Marie Pédrot2014-03-08
* Also use HMaps in KNmap.Gravatar Pierre-Marie Pédrot2014-03-08
* Using Hashmaps by default in constant and inductive maps. This changes fold andGravatar Pierre-Marie Pédrot2014-03-07
* Inductive maps in Environ now use HMap.Gravatar Pierre-Marie Pédrot2014-03-06
* Fix typo in comment.Gravatar Maxime Dénès2014-03-05
* Using HMaps in Safe_env.environments, hopefully improving performances.Gravatar Pierre-Marie Pédrot2014-03-05
* Canary testing absence of generic equality for KerNamesGravatar Pierre-Marie Pédrot2014-03-05
* Lazily computed hash in KerName.t.Gravatar Pierre-Marie Pédrot2014-03-05
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Correct handling of hashconsing of constraint sets. The previous implementationGravatar Pierre-Marie Pédrot2014-03-05
* Fixing pervasives equalities in Vconv.Gravatar Pierre-Marie Pédrot2014-03-04
* Fixing Pervasives.equality in extraction.Gravatar Pierre-Marie Pédrot2014-03-03
* Fixing pervasive equalities. In particular, I removed the code that deletedGravatar Pierre-Marie Pédrot2014-03-03
* Removing generic hashes in kernel.Gravatar Pierre-Marie Pédrot2014-03-03
* Kernel names are implemented using records.Gravatar Pierre-Marie Pédrot2014-03-03
* Fixing generic hashes and replacing them with proper ones.Gravatar Pierre-Marie Pédrot2014-03-03
* Fixing generic Hashtbl.hash in Constr.Gravatar Pierre-Marie Pédrot2014-03-02
* Hunting pervasive equality in native compiler. It seems they were used forGravatar Pierre-Marie Pédrot2014-03-01
* STM: when batch compiling a vo, assert we behave conservativelyGravatar Enrico Tassi2014-02-26
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* remoteCounter: backup/restoreGravatar Enrico Tassi2014-02-26
* univ: removing dead codeGravatar Enrico Tassi2014-02-26
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
* Optimization in kernel/vars.ml: directly allocate a fixed-size block in theGravatar Pierre-Marie Pédrot2014-02-20
* Made Pre_env.lazy_val opaque.Gravatar Pierre-Marie Pédrot2014-02-11
* Small optimizations in Closure:Gravatar Pierre-Marie Pédrot2014-02-09
* Tracking memory misallocation by trying to improve sharing.Gravatar Pierre-Marie Pédrot2014-02-03
* Allocation-friendly mapping functions in Nametab.Gravatar Pierre-Marie Pédrot2014-02-03
* Relaxing the sort elimination check to allow for let-bindings in arities.Gravatar Maxime Dénès2014-01-18
* Christmas is over...Gravatar Maxime Dénès2014-01-15
* STM: additional fix for STM + vm_computeGravatar Enrico Tassi2014-01-07
* STM: fix worker crash when doing vm_computeGravatar Enrico Tassi2014-01-06
* Proof_using: new syntax + suggestionGravatar Enrico Tassi2014-01-05
* Environ: export API to transitively close a set of section variablesGravatar Enrico Tassi2014-01-05
* Paral-ITP: cleanup of command line flags and more conservative defaultGravatar Enrico Tassi2014-01-05
* .vi files: .vo files without proofsGravatar Enrico Tassi2014-01-04
* kernel: save in aux the list of section variables usedGravatar Enrico Tassi2014-01-04
* Remove obsolete comment about Let being processed synchronouslyGravatar Enrico Tassi2014-01-04
* Support for evars and metas in native compiler.Gravatar Maxime Dénès2013-12-30
* Avoid generating .ml files in native compiler.Gravatar Maxime Dénès2013-12-29
* Got rid of unused lazy flag in the native compiler.Gravatar Maxime Dénès2013-12-29
* Revert "Partial revert of r16711"Gravatar Maxime Dénès2013-12-28
* Removing native_name reference from constant_body.Gravatar Maxime Dénès2013-12-28
* STM: capture type checking error (Closes: 3195)Gravatar Enrico Tassi2013-12-24
* Qed: feedback when type checking is doneGravatar Enrico Tassi2013-12-24
* Tentative fix of the guardedness checker by Christine and me. All stdlib and ...Gravatar Matthieu Sozeau2013-12-17
* A few fixes to the build system (mostly for ocamlbuild)Gravatar Pierre Letouzey2013-12-16
* Do not overallocate closures' named environments in infos. Modifying the accessGravatar Pierre-Marie Pédrot2013-12-15
* Reduction: every n iterations a slaves process checks for interruptionGravatar Enrico Tassi2013-11-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 11:29:21 +0000