| Age | Commit message (Expand) | Author |
|---|
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2016-01-17 | Universes algorithm : clarified comments | Jacques-Henri Jourdan |
| 2015-11-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-11-27 | Univs: entirely disallow instantiation of polymorphic constants with | Matthieu Sozeau |
| 2015-11-23 | Fix output of universe arcs. (Fix bug #4422) | Guillaume Melquiond |
| 2015-11-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-11-04 | Univs: update refman, better printers for universe contexts. | Matthieu Sozeau |
| 2015-10-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-28 | Adds support for the virtual machine to perform reduction of universe polymor... | Gregory Malecha |
| 2015-10-09 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-08 | Univs: fix bug #3807 | Matthieu Sozeau |
| 2015-10-06 | Splitting kernel universe code in two modules. | Pierre-Marie Pédrot |
| 2015-10-05 | Univs: fix bug #4288, Print Sorted generated backward < constraints. | Matthieu Sozeau |
| 2015-10-02 | Univs: fix bug #4251, handling of template polymorphic constants. | Matthieu Sozeau |
| 2015-10-02 | Univs (kernel) adapt to new invariants | Matthieu Sozeau |
| 2015-10-02 | Forcing i > Set for global universes (incomplete) | Matthieu Sozeau |
| 2015-10-02 | Universes: enforce Set <= i for all Type occurrences. | Matthieu Sozeau |
| 2015-08-02 | Reverting 16 last commits, committed mistakenly using the wrong push command. | Hugo Herbelin |
| 2015-08-02 | A patch renaming equal into eq in the module dealing with | Hugo Herbelin |
| 2015-07-16 | Modules: fix bug #4294 | Matthieu Sozeau |
| 2015-07-01 | Further simplification of the graph traversal in Univ. | Pierre-Marie Pédrot |
| 2015-06-24 | Less closures makes the GC happy. | Pierre-Marie Pédrot |
| 2015-06-23 | Less closures makes the GC happy. | Pierre-Marie Pédrot |
| 2015-02-11 | Fixing bug #4019, and checker blow-up at once. | Pierre-Marie Pédrot |
| 2015-02-11 | Clarifying the implementation of universe hashconsing. | Pierre-Marie Pédrot |
| 2015-01-28 | Fixing bug #3931. | Pierre-Marie Pédrot |
| 2015-01-17 | Univs: proper printing of global and local universe names (only | Matthieu Sozeau |
| 2015-01-17 | Make native compiler handle universe polymorphic definitions. | Maxime Dénès |
| 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-07 | Aligning printing of universe constraints. | Hugo Herbelin |
| 2014-12-21 | Dead code in Univ. | Pierre-Marie Pédrot |
| 2014-12-18 | Cleaning up universe list implementation in Univ. | Pierre-Marie Pédrot |
| 2014-12-17 | Ensuring the good invariants of hashcons table generation in the API. | Pierre-Marie Pédrot |
| 2014-12-14 | Fix merging of name maps in union of universe contexts. | Matthieu Sozeau |
| 2014-10-02 | Implement module subtyping for polymorphic constants (errors on | Matthieu Sozeau |
| 2014-09-18 | Clean a bit of univ.ml, add credits. | Matthieu Sozeau |
| 2014-09-05 | Fix checker treatment of inductives using subst_instances instead of subst_un... | Matthieu Sozeau |
| 2014-09-04 | Fix bug #3559, ensuring a canonical order of universe level quantifications when | Matthieu Sozeau |
| 2014-08-30 | Simplify even further the declaration of primitive projections, | Matthieu Sozeau |
| 2014-08-18 | Fix pretty-printing of the graph in Print Sorted Universes. Type.0 was larger... | Matthieu Sozeau |
| 2014-08-09 | Adding a primitive to merge ContextSets which is more efficient when one | Pierre-Marie Pédrot |
| 2014-08-09 | Cleaning up interface of ContextSet. | Pierre-Marie Pédrot |
| 2014-08-04 | Fixing semantics of Univ.Level.equal. | Pierre-Marie Pédrot |
| 2014-08-03 | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau |
| 2014-07-31 | Useless export of Instance.eqeq. We hashcons everything before calling this | Pierre-Marie Pédrot |
| 2014-07-30 | Avoid hconsing instances during appends and conversions from/to arrays. | Matthieu Sozeau |
| 2014-07-21 | Universe level maps use HMaps. | Pierre-Marie Pédrot |
| 2014-07-21 | Cleanup substitution inside universe instances, only done through subst_fn now, | Matthieu Sozeau |
