| Age | Commit message (Expand) | Author |
|---|
| 2013-10-29 | Optimizing universes: tail-rec, allocation friendly [compare_leq]. | ppedrot |
| 2013-10-28 | Native compiler: library compilation errors are now non fatal. | mdenes |
| 2013-10-27 | More sharing in Constr.map_with_binders. | ppedrot |
| 2013-10-24 | More monomorphic List.mem + List.assoc + ... | letouzey |
| 2013-10-24 | inductive.ml : get rid of some obvious (Lazy.force (lazy t)) | letouzey |
| 2013-10-24 | Rtree : cleanup of the comparing code | letouzey |
| 2013-10-24 | Specializing hash functions for widely used types. | ppedrot |
| 2013-10-24 | Turn many List.assoc into List.assoc_f | letouzey |
| 2013-10-23 | cList: a few alternative to hashtbl-based uniquize, distinct, subset | letouzey |
| 2013-10-23 | cList.index is now cList.index_f, same for index0 | letouzey |
| 2013-10-23 | cList: set-as-list functions are now with an explicit comparison | letouzey |
| 2013-10-23 | Optimizing Vars.replace_vars | ppedrot |
| 2013-10-22 | Removing some generic equalities. | ppedrot |
| 2013-10-22 | Various optimizations in Constr, such as term sharing and allocation | ppedrot |
| 2013-10-18 | Future: ported to Ephemeron + exception enhancing | gareuselesinge |
| 2013-10-04 | Fix comment for new string syntax (OCaml trunk). | xclerc |
| 2013-10-03 | A shallow copy of a pre_env does not contain the vm cache | gareuselesinge |
| 2013-09-27 | Removing a bunch of generic equalities. | ppedrot |
| 2013-09-19 | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc |
| 2013-09-18 | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot |
| 2013-09-14 | Slightly more compact representation of 'a substituted type, | ppedrot |
| 2013-08-30 | ind_tables: properly handling side effects | gareuselesinge |
| 2013-08-30 | Remove Obj.magic from safe typing | gareuselesinge |
| 2013-08-25 | Added a more efficient way to recover the domain of a map. | ppedrot |
| 2013-08-25 | Replacing lists by sets in clear tactic. | ppedrot |
| 2013-08-23 | Fix computation of discharged hyps for inductive types forgetting the conclus... | msozeau |
| 2013-08-22 | Misc changes around coqtop.ml : | letouzey |
| 2013-08-22 | More complete hashcons : lists (dirpath), arrays (constr) | letouzey |
| 2013-08-20 | Partial revert of r16711 | letouzey |
| 2013-08-20 | Universe counters on slaves are in sync with master | gareuselesinge |
| 2013-08-20 | Declarations.mli: reorganization of modular structures | letouzey |
| 2013-08-20 | Declareops + Modops : more clever substitutions | letouzey |
| 2013-08-20 | Mod_typing : code cleanup | letouzey |
| 2013-08-20 | Safe_typing code refactoring | letouzey |
| 2013-08-20 | Attempt to restore hash-consing of opaque terms | letouzey |
| 2013-08-19 | Cleanup code in term_typing | gareuselesinge |
| 2013-08-19 | abstract+Defined: create opaque sub proofs (as pre-ParalITP) | gareuselesinge |
| 2013-08-08 | get rid of closures in global/proof state | gareuselesinge |
| 2013-08-08 | enhance marshallable option for freeze (minor TODO in safe_typing) | gareuselesinge |
| 2013-08-08 | State Transaction Machine | gareuselesinge |
| 2013-08-04 | Fixing #2846: Uncaught exception Reduction.NotArity. | ppedrot |
| 2013-08-04 | Removing useless casts between arrays and lists. | ppedrot |
| 2013-08-03 | Small fixes due to the arrival of OCaml 3.12. | ppedrot |
| 2013-07-17 | Modops.destr_functor without useless env | letouzey |
| 2013-07-17 | Safe_typing: minor factorisation | letouzey |
| 2013-07-10 | Added a Register Inline command for the native compiler. Will be ported to th... | mdenes |
| 2013-07-06 | Fixing a bug in the native compiler, introduced by r16363, leading to undefined | mdenes |
| 2013-05-30 | comments in mli | pboutill |
| 2013-05-14 | Delayed the computation of parameters in sort polymorphism of | herbelin |
| 2013-05-14 | Replacing Id.check with Id.is_valid, as its sole use was under | ppedrot |
