aboutsummaryrefslogtreecommitdiff
path: root/checker/checker.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/checker.ml')
-rw-r--r--checker/checker.ml2
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"