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 /checker | |
| 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 'checker')
| -rw-r--r-- | checker/checker.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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" |