diff options
Diffstat (limited to 'dev/top_printers.ml')
| -rw-r--r-- | dev/top_printers.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index e3addd6f04..b35d5d4899 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -46,7 +46,7 @@ let ppdir dir = pp (pr_dirpath dir) let ppmp mp = pp(str (string_of_mp mp)) let ppcon con = pp(pr_con con) let ppkn kn = pp(pr_kn kn) -let ppsp sp = pp(pr_sp sp) +let ppsp sp = pp(pr_path sp) let ppqualid qid = pp(pr_qualid qid) let ppclindex cl = pp(Classops.pr_cl_index cl) |