aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Fix universe handling (bug introduced in vi2vo commit)Gravatar Enrico Tassi2014-04-08
* Fixing coqchk. It was my fault, I misused canonical and user equalitiesGravatar Pierre-Marie Pédrot2014-04-04
* Missing equalities in Names-like structures.Gravatar Pierre-Marie Pédrot2014-03-20
* Adding a Print Strategy vernacular command. It allows to check theGravatar Pierre-Marie Pédrot2014-03-19
* Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it hadGravatar Pierre-Marie Pédrot2014-03-14
* vi2vo: universes handling finally fixedGravatar Enrico Tassi2014-03-11
* Fix (3243): univ constraints of module subtyping were not propagatedGravatar Enrico Tassi2014-03-11
* Useless Array.to_list in Typeops.Gravatar Pierre-Marie Pédrot2014-03-10
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 12:07:36 +0000