From 237b569dd6539fc1730dbd1dda29f83e24ef8d0c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
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/printer.mli | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'printing/printer.mli')

diff --git a/printing/printer.mli b/printing/printer.mli
index 75ab1722db..6b9c70815d 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -79,12 +79,11 @@ val pr_constr_pattern      : constr_pattern -> std_ppcmds
 
 val pr_cases_pattern       : cases_pattern -> std_ppcmds
 
-val pr_sort                : sorts -> std_ppcmds
+val pr_sort                : evar_map -> sorts -> std_ppcmds
 
 (** Universe constraints *)
 
 val pr_polymorphic         : bool -> std_ppcmds
-val pr_univ_cstr           : Univ.constraints -> std_ppcmds
 val pr_universe_ctx        : Univ.universe_context -> std_ppcmds
 
 (** Printing global references using names as short as possible *)
-- 
cgit v1.2.3