From 3bcca0aecb368a723d247d1f8b2348790bc87035 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Sat, 17 Jan 2015 20:17:17 +0530
Subject: Univs: proper printing of global and local universe names (only
 printing functions touched in the kernel).

---
 printing/pptactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing/pptactic.ml')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 7cc193a8d..f8264e5af 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1451,7 +1451,7 @@ let () =
     (pr_clauses (Some true) (fun id -> pr_lident (Loc.ghost,id)))
   ;
   Genprint.register_print0 Constrarg.wit_sort
-    pr_glob_sort pr_glob_sort pr_sort;
+    pr_glob_sort pr_glob_sort (pr_sort Evd.empty);
   Genprint.register_print0
     Constrarg.wit_uconstr
     Ppconstr.pr_constr_expr
-- 
cgit v1.2.3