| Age | Commit message (Expand) | Author |
|---|
| 2016-06-18 | Adding a local type-in-type flag in kernel declarations. | Pierre-Marie Pédrot |
| 2016-02-15 | CLEANUP: Simplifying the changes done in "kernel/*" | Matej Kosik |
| 2016-02-09 | CLEANUP: Context.{Rel,Named}.Declaration.t | Matej Kosik |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2016-01-11 | CLEANUP: kernel/context.ml{,i} | Matej Kosik |
| 2015-10-06 | Splitting kernel universe code in two modules. | Pierre-Marie Pédrot |
| 2015-10-02 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-02 | Univs: module constraints move to universe contexts as they might | Matthieu Sozeau |
| 2015-10-02 | Forcing i > Set for global universes (incomplete) | Matthieu Sozeau |
| 2015-09-10 | Assertion checking that invariant enforced by 0f8d1b92 always holds. | Maxime Dénès |
| 2015-08-02 | Fixing pop_rel_context. | Hugo Herbelin |
| 2015-08-02 | Reverting 16 last commits, committed mistakenly using the wrong push command. | Hugo Herbelin |
| 2015-08-02 | Fixing pop_rel_context | Hugo Herbelin |
| 2015-07-10 | Option -type-in-type: added support in checker and making it contaminating | Hugo Herbelin |
| 2015-03-25 | Fix vm compiler to refuse to compile code making use of inductives with | Matthieu Sozeau |
| 2015-01-15 | Correct restriction of vm_compute when handling universe polymorphic | Matthieu Sozeau |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2015-01-11 | Declarations.mli refactoring: module_type_body = module_body | Pierre Letouzey |
| 2014-11-12 | Cleaner interfaces for linking locations of native compiler. | Maxime Dénès |
| 2014-10-24 | Fix retroknowledge for int31 division. | Maxime Dénès |
| 2014-10-13 | library/opaqueTables: enable their use in interactive mode | Enrico Tassi |
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau |
| 2014-09-24 | Make the retroknowledge marshalable. | Arnaud Spiwack |
| 2014-09-13 | Providing a -type-in-type option for collapsing the universe hierarchy. | Hugo Herbelin |
| 2014-08-03 | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
| 2014-06-13 | Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284). | Hugo Herbelin |
| 2014-06-04 | - Fix hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 2014-05-06 | Adapt universe polymorphic branch to new handling of futures for delayed proofs. | Matthieu Sozeau |
| 2014-05-06 | - Rename eq to equal in Univ, document new modules, set interfaces. | Matthieu Sozeau |
| 2014-05-06 | Fix interface for template polymorphism, cleaning up code in all typing algor... | Matthieu Sozeau |
| 2014-05-06 | Initial work on reintroducing old-style polymorphism for compatibility (the s... | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-09 | Int31 decompilation in native compiler was still partial. Now fixed. | Maxime Dénès |
| 2014-04-09 | Machine arithmetic operations for native compiler. | Maxime Dénès |
| 2014-04-09 | Full support for int31 values in native compiler. | Maxime Dénès |
| 2014-04-09 | Partial support for open terms in int31. | Maxime Dénès |
| 2014-03-14 | Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it had | Pierre-Marie Pédrot |
| 2014-03-07 | Using Hashmaps by default in constant and inductive maps. This changes fold and | Pierre-Marie Pédrot |
| 2014-03-06 | Inductive maps in Environ now use HMap. | Pierre-Marie Pédrot |
| 2014-03-05 | Using HMaps in Safe_env.environments, hopefully improving performances. | Pierre-Marie Pédrot |
| 2014-02-26 | Lazyconstr -> Opaqueproof | Enrico Tassi |
| 2014-02-03 | Tracking memory misallocation by trying to improve sharing. | Pierre-Marie Pédrot |
| 2014-01-05 | Environ: export API to transitively close a set of section variables | Enrico Tassi |
| 2013-12-28 | Removing native_name reference from constant_body. | Maxime Dénès |
| 2013-11-15 | Revert "Fast lookup_named in environments, based on maps instead of lists." | ppedrot |
| 2013-11-13 | Fast lookup_named in environments, based on maps instead of lists. | ppedrot |
| 2013-10-31 | Conv_orable made functional and part of pre_env | gareuselesinge |
