From f821438c9759c4788d597688b25cb78f2a2c01c4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 5 Jan 2021 21:54:12 +0100
Subject: 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.
---
 dev/top_printers.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

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
-- 
cgit v1.2.3