From de648c72a79ae5ba35db166575669ca465b11770 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Thu, 1 Oct 2015 18:41:49 +0200
Subject: Univs: fix checker generating undeclared universes.

---
 checker/reduction.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker/reduction.ml')

diff --git a/checker/reduction.ml b/checker/reduction.ml
index 8ddeea2a2..384d883ea 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -175,7 +175,7 @@ let sort_cmp env univ pb s0 s1 =
         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
+            Printf.eprintf "sort_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;
-- 
cgit v1.2.3