From 2947dd269744bcb9b0a487e262e8f21bb2a382eb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 28 Jan 2015 20:12:42 +0100
Subject: Fixing bug #3931.

---
 kernel/univ.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3