aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-13 18:43:02 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-13 18:45:41 +0100
commitc571cdbbcac5cb4b4a5a19ab2f7ac51222316292 (patch)
tree2ec7070bc8d58ee4b6fd0734ea41964243a0f2ba /dev
parent6bd240fce21c172680a0cec5346b66e08c76418a (diff)
[api] Another large deprecation, `Nameops`
Diffstat (limited to 'dev')
-rw-r--r--dev/top_printers.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index e48abce1c..b4c8ae33c 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))