| Commit message (Expand) | Author | Age |
... | |
* | Modules: fix bug #4294 | Matthieu Sozeau | 2015-07-16 |
* | Further simplification of the graph traversal in Univ. | Pierre-Marie Pédrot | 2015-07-01 |
* | Less closures makes the GC happy. | Pierre-Marie Pédrot | 2015-06-24 |
* | Less closures makes the GC happy. | Pierre-Marie Pédrot | 2015-06-23 |
* | 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-02-11 |
* | Fixing bug #3931. | Pierre-Marie Pédrot | 2015-01-28 |
* | 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-17 |
* | Correct restriction of vm_compute when handling universe polymorphic | Matthieu Sozeau | 2015-01-15 |
* | Update headers. | Maxime Dénès | 2015-01-12 |
* | Aligning printing of universe constraints. | Hugo Herbelin | 2015-01-07 |
* | Dead code in Univ. | Pierre-Marie Pédrot | 2014-12-21 |
* | Cleaning up universe list implementation in Univ. | Pierre-Marie Pédrot | 2014-12-18 |
* | Ensuring the good invariants of hashcons table generation in the API. | Pierre-Marie Pédrot | 2014-12-17 |
* | Fix merging of name maps in union of universe contexts. | Matthieu Sozeau | 2014-12-14 |
* | Implement module subtyping for polymorphic constants (errors on | Matthieu Sozeau | 2014-10-02 |
* | Clean a bit of univ.ml, add credits. | Matthieu Sozeau | 2014-09-18 |
* | Fix checker treatment of inductives using subst_instances instead of subst_un... | Matthieu Sozeau | 2014-09-05 |
* | Fix bug #3559, ensuring a canonical order of universe level quantifications when | Matthieu Sozeau | 2014-09-04 |
* | Simplify even further the declaration of primitive projections, | Matthieu Sozeau | 2014-08-30 |
* | Fix pretty-printing of the graph in Print Sorted Universes. Type.0 was larger... | Matthieu Sozeau | 2014-08-18 |
* | 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-09 |
* | Fixing semantics of Univ.Level.equal. | Pierre-Marie Pédrot | 2014-08-04 |
* | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau | 2014-08-03 |
* | Useless export of Instance.eqeq. We hashcons everything before calling this | Pierre-Marie Pédrot | 2014-07-31 |
* | Avoid hconsing instances during appends and conversions from/to arrays. | Matthieu Sozeau | 2014-07-30 |
* | 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 | 2014-07-21 |
* | Cleanup code related to the constraint solving, which sits now outside the | Matthieu Sozeau | 2014-07-03 |
* | Properly compute the transitive closure of the system of constraints | Matthieu Sozeau | 2014-07-03 |
* | Add toplevel commands to declare global universes and constraints. | Matthieu Sozeau | 2014-07-01 |
* | Fix type_of_inductive_knowing_conclusion, relying on an actually broken univ_... | Matthieu Sozeau | 2014-06-25 |
* | Code factorization in LMap. | Pierre-Marie Pédrot | 2014-06-18 |
* | Code cleaning in Univ. | Pierre-Marie Pédrot | 2014-06-12 |
* | In generalized rewrite, avoid retyping completely and constantly the conclusi... | Matthieu Sozeau | 2014-06-11 |
* | Fixing Sorting Universes in a world where le and lt constraints may be | Pierre-Marie Pédrot | 2014-06-10 |
* | Compute the trace of a universe inconsistency only when explicitly required | Pierre-Marie Pédrot | 2014-06-10 |
* | Made explanations for universe inconsistencies optional. They are only used | Pierre-Marie Pédrot | 2014-06-10 |
* | Specialize the type of [Univ.compare_neq] so that it is clear it is only used | Pierre-Marie Pédrot | 2014-06-10 |
* | Imperatively check touched universes in compare_neq functions. This ensures | Pierre-Marie Pédrot | 2014-06-10 |
* | - Fix substitution of universes which needlessly hashconsed existing universes. | Matthieu Sozeau | 2014-06-10 |
* | Oops, one refactoring was not compiled. | Matthieu Sozeau | 2014-06-10 |
* | More cleanup/reorganizing of univ.ml to separate constraint/universe handling... | Matthieu Sozeau | 2014-06-10 |
* | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau | 2014-06-10 |
* | Remove unused function in univ | Matthieu Sozeau | 2014-06-10 |
* | Flattening Level module structure in Univ. | Pierre-Marie Pédrot | 2014-06-09 |
* | Function in Univ uselessly exported. | Pierre-Marie Pédrot | 2014-06-08 |
* | Make kernel reduction code parametric over the handling of universes, | Matthieu Sozeau | 2014-06-06 |