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 /dev | |
| 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 'dev')
| -rw-r--r-- | dev/top_printers.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 6ce347ad59..e70777bd2c 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -240,7 +240,7 @@ let ppuniverseconstraints c = pp (UnivProblem.Set.pr c) let ppuniverse_context_future c = let ctx = Future.force c in ppuniverse_context ctx -let ppuniverses u = pp (UGraph.pr_universes Level.pr u) +let ppuniverses u = pp (UGraph.pr_universes Level.pr (UGraph.repr u)) let ppnamedcontextval e = let env = Global.env () in let sigma = Evd.from_env env in |