From c571cdbbcac5cb4b4a5a19ab2f7ac51222316292 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 13 Nov 2017 18:43:02 +0100
Subject: [api] Another large deprecation, `Nameops`

---
 dev/top_printers.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index e48abce1c4..b4c8ae33ca 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -14,7 +14,6 @@ open Pp
 open Names
 open Libnames
 open Globnames
-open Nameops
 open Univ
 open Environ
 open Printer
@@ -38,7 +37,7 @@ let ppfuture kx = pp (Future.print (fun _ -> str "_") kx)
 
 (* name printers *)
 let ppid id = pp (Id.print id)
-let pplab l = pp (pr_lab l)
+let pplab l = pp (Label.print l)
 let ppmbid mbid = pp (str (MBId.debug_to_string mbid))
 let ppdir dir = pp (pr_dirpath dir)
 let ppmp mp = pp(str (ModPath.debug_to_string mp))
-- 
cgit v1.2.3