aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/univ.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 08e9fee051..492762df39 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -2064,7 +2064,7 @@ let explain_universe_inconsistency prl (o,u,v,p) =
(spc() ++ str "= " ++ pr_uni u))
in
str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++
- pr_rel o ++ spc() ++ pr_uni v ++ reason ++ str")"
+ pr_rel o ++ spc() ++ pr_uni v ++ reason
let compare_levels = Level.compare
let eq_levels = Level.equal