From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Wed, 15 Jul 2015 10:36:12 +0200
Subject: Imported Upstream version 8.5~beta2+dfsg

---
 checker/reduction.ml | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'checker/reduction.ml')

diff --git a/checker/reduction.ml b/checker/reduction.ml
index 185c6edf..28fdb130 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -169,7 +169,15 @@ let sort_cmp univ pb s0 s1 =
 	  (match pb with
             | CONV -> Univ.check_eq univ u1 u2
 	    | CUMUL -> Univ.check_leq univ u1 u2)
-        then raise NotConvertible
+        then begin
+          if !Flags.debug then begin
+            let op = match pb with CONV -> "=" | CUMUL -> "<=" in
+            Printf.eprintf "cort_cmp: %s\n%!" Pp.(string_of_ppcmds
+              (str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
+               ++ Univ.pr_universes univ))
+          end;
+          raise NotConvertible
+        end
     | (_, _) -> raise NotConvertible
 
 let rec no_arg_available = function
-- 
cgit v1.2.3