aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/uGraph.mli
Commit message (Collapse)AuthorAge
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
|
* Cleaning up the implementation of module subtyping in the kernel.Gravatar Pierre-Marie Pédrot2017-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 unificationGravatar Maxime Dénès2017-05-23
|\
* | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| |
| * Fast path when checking equality of universe levels in UState.Gravatar Pierre-Marie Pédrot2017-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.Gravatar Pierre-Marie Pédrot2015-10-06
1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity.