aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-11-16 16:06:17 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-11-16 16:06:17 +0100
commit0786ae361cb5f134e91d790d6c096f84535b19ec (patch)
treec4aeb3ac1a9c750ecb8e5d79abf218fecab2f774 /dev
parent11d895262e49b4c9f371e38c9e4436cead7001f4 (diff)
parented0c434a05a929a659e43aed80ab7c8179a7daa3 (diff)
Merge PR #6148: [api] Another large deprecation, `Nameops` and friends.
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))