diff options
| author | coqbot-app[bot] | 2021-01-07 09:32:34 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-07 09:32:34 +0000 |
| commit | 331592e05f6f222da40489a94abdcdd3ef4b6394 (patch) | |
| tree | 190e7e1202e48bafe6cd137910d7449f6d814850 /checker | |
| parent | ad9fdf76897ada659dc1ca6d2d931452f6361f93 (diff) | |
| parent | f821438c9759c4788d597688b25cb78f2a2c01c4 (diff) | |
Merge PR #13718: Move printing and sorting out of AcyclicGraph
Reviewed-by: SkySkimmer
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" |