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.
---
 checker/checker.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker')

diff --git a/checker/checker.ml b/checker/checker.ml
index 08d92bb7b3..bdfc5f07be 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -289,7 +289,7 @@ let explain_exn = function
                              Constr.debug_print a ++ fnl ());
         Feedback.msg_notice (str"====== universes ====" ++ fnl () ++
                              (UGraph.pr_universes Univ.Level.pr
-                                (ctx.Environ.env_stratification.Environ.env_universes)));
+                                (UGraph.repr (ctx.Environ.env_stratification.Environ.env_universes))));
         str "CantApplyBadType at argument " ++ int n
       | CantApplyNonFunctional _ -> str"CantApplyNonFunctional"
       | IllFormedRecBody _ -> str"IllFormedRecBody"
-- 
cgit v1.2.3