aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2014-03-11vi2vo: universes handling finally fixedEnrico Tassi
2014-03-11Fix (3243): univ constraints of module subtyping were not propagatedEnrico Tassi
2014-03-10Useless Array.to_list in Typeops.Pierre-Marie Pédrot
2014-03-08Using HMaps in global references.Pierre-Marie Pédrot
2014-03-08Also use HMaps in KNmap.Pierre-Marie Pédrot
2014-03-07Using Hashmaps by default in constant and inductive maps. This changes fold andPierre-Marie Pédrot
2014-03-06Inductive maps in Environ now use HMap.Pierre-Marie Pédrot
2014-03-05Fix typo in comment.Maxime Dénès
2014-03-05Using HMaps in Safe_env.environments, hopefully improving performances.Pierre-Marie Pédrot
2014-03-05Canary testing absence of generic equality for KerNamesPierre-Marie Pédrot
2014-03-05Lazily computed hash in KerName.t.Pierre-Marie Pédrot
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-05Correct handling of hashconsing of constraint sets. The previous implementationPierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:02:49 +0000