From 9834fe8ac933230607eb33c9cbbaa68a7b13f4fe Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 17 Oct 2012 02:35:08 +0000
Subject: univ inconsistency error message gives evidence of a cycle

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15898 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 checker/checker.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'checker')

diff --git a/checker/checker.ml b/checker/checker.ml
index 8389803fcb..8e0a2a1e5c 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -252,12 +252,12 @@ let rec explain_exn = function
       hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report ())
   | Sys.Break ->
       hov 0 (fnl () ++ str "User interrupt.")
-  | Univ.UniverseInconsistency (o,u,v) ->
+  | Univ.UniverseInconsistency (o,u,v,_) ->
       let msg =
 	if !Flags.debug (*!Constrextern.print_universes*) then
-	  spc() ++ str "(cannot enforce" ++ spc() ++ (*Univ.pr_uni u ++*) spc() ++
+	  spc() ++ str "(cannot enforce" ++ spc() ++ Univ.pr_uni u ++ spc() ++
           str (match o with Univ.Lt -> "<" | Univ.Le -> "<=" | Univ.Eq -> "=")
-	  ++ spc() ++ (*Univ.pr_uni v ++*) str")"
+	  ++ spc() ++ Univ.pr_uni v ++ str")"
 	else
 	  mt() in
       hov 0 (str "Error: Universe inconsistency" ++ msg ++ str ".")
-- 
cgit v1.2.3