aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/top_printers.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 0f496d3b9f..df5f054692 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -39,7 +39,7 @@ let ppfuture kx = pp (Future.print (fun _ -> str "_") kx)
let ppid id = pp (Id.print id)
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 ppdir dir = pp (DirPath.print dir)
let ppmp mp = pp(str (ModPath.debug_to_string mp))
let ppcon con = pp(Constant.debug_print con)
let ppproj con = pp(Constant.debug_print (Projection.constant con))