diff options
| author | Pierre-Marie Pédrot | 2021-01-05 21:54:12 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-06 11:19:21 +0100 |
| commit | f821438c9759c4788d597688b25cb78f2a2c01c4 (patch) | |
| tree | 795eb563376b22f226fca0ab80b7b26ed61bca28 /kernel/nativelib.mli | |
| parent | bdd186a7d6fc6e413e1b575085402f3c88fa5c23 (diff) | |
Further pushing up the printing and sorting of universes.
We expose the representation function in UGraph and change the printer
signature to work over the representation instead of the abstract type.
Similarly, the topological sorting algorithm is moved to Vernacentries.
It is now even simpler.
Diffstat (limited to 'kernel/nativelib.mli')
0 files changed, 0 insertions, 0 deletions