Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fix restrict_universe_context | 2018-05-30 | |
| | |||
* | universe normalisation: put equivalence class partition in UGraph | 2018-04-13 | |
| | | | | ie don't go through having Eq constraints but directly to the unionfind. | ||
* | Replace invalid tag @raises in ocamldoc comments with @raise | 2018-03-05 | |
| | |||
* | Update headers following #6543. | 2018-02-27 | |
| | |||
* | [api] Remove yet another type alias. | 2017-12-09 | |
| | |||
* | [api] Move structures deprecated in the API to the core. | 2017-11-06 | |
| | | | | We do up to `Term` which is the main bulk of the changes. | ||
* | deprecate Pp.std_ppcmds type alias | 2017-07-27 | |
| | |||
* | Cleaning up the implementation of module subtyping in the kernel. | 2017-07-11 | |
| | | | | | | | | We export a function in UGraph to check that a polymorphic instance is a subtype of another, instead of rolling up our own in module code. We also add a few tests for module subtyping in presence of polymorphic constants. | ||
* | Merge PR#518: Faster universe unification | 2017-05-23 | |
|\ | |||
* | | Remove some unused values and types | 2017-04-27 | |
| | | |||
| * | Fast path when checking equality of universe levels in UState. | 2017-04-27 | |
|/ | | | | | We export the relevant level equality function in UGraph which is way faster than checking that each one is smaller than the other as universes. | ||
* | Splitting kernel universe code in two modules. | 2015-10-06 | |
1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity. |