aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2014-04-09Fix exponential behavior in native compiler with retroknowledge.Maxime Dénès
2014-04-09Fix name of some Int31 operations in native compiler.Maxime Dénès
2014-04-09Optimizing Int31 support in native compiler, by not taggingMaxime Dénès
2014-04-09Int31 decompilation in native compiler was still partial. Now fixed.Maxime Dénès
2014-04-09Machine arithmetic operations for native compiler.Maxime Dénès
2014-04-09Full support for int31 values in native compiler.Maxime Dénès
2014-04-09Partial support for open terms in int31.Maxime Dénès
2014-04-09Had to split Nativelambda in two files because of RetroknowledgeMaxime Dénès
2014-04-09Int31 literals in native compiler.Maxime Dénès
2014-04-09Uint31 support.Maxime Dénès
2014-04-08Fix universe handling (bug introduced in vi2vo commit)Enrico Tassi
2014-04-04Fixing coqchk. It was my fault, I misused canonical and user equalitiesPierre-Marie Pédrot
2014-03-20Missing equalities in Names-like structures.Pierre-Marie Pédrot
2014-03-19Adding a Print Strategy vernacular command. It allows to check thePierre-Marie Pédrot
2014-03-14Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it hadPierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 08:40:59 +0000