From 23f0f5fe6b510d2ab91a2917eb895faa479d9fcf Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Sun, 19 Nov 2017 07:42:16 +0100
Subject: [api] Miscellaneous consolidation + moves to engine.

We deprecate a few functions that were deprecated in the comments plus
we place `Nameops` and `Univops` in engine where they do seem to
belong in the large picture of code organization.
---
 printing/ppvernac.ml | 6 +++---
 printing/prettyp.ml  | 4 ++--
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 143f9ddcc..e897b1938 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -447,7 +447,7 @@ open Decl_kinds
     | PrintGrammar ent ->
       keyword "Print Grammar" ++ spc() ++ str ent
     | PrintLoadPath dir ->
-      keyword "Print LoadPath" ++ pr_opt pr_dirpath dir
+      keyword "Print LoadPath" ++ pr_opt DirPath.print dir
     | PrintModules ->
       keyword "Print Modules"
     | PrintMLLoadPath ->
@@ -518,7 +518,7 @@ open Decl_kinds
       in
       keyword cmd ++ spc() ++ pr_smart_global qid
     | PrintNamespace dp ->
-      keyword "Print Namespace" ++ pr_dirpath dp
+      keyword "Print Namespace" ++ DirPath.print dp
     | PrintStrategy None ->
       keyword "Print Strategies"
     | PrintStrategy (Some qid) ->
@@ -964,7 +964,7 @@ open Decl_kinds
                keyword "LoadPath" ++ spc() ++ qs s ++
                (match d with
                  | None -> mt()
-                 | Some dir -> spc() ++ keyword "as" ++ spc() ++ pr_dirpath dir))
+                 | Some dir -> spc() ++ keyword "as" ++ spc() ++ DirPath.print dir))
         )
       | VernacRemoveLoadPath s ->
         return (keyword "Remove LoadPath" ++ qs s)
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index e2d23ce7b..060cf6fc7 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -366,7 +366,7 @@ let pr_located_qualid = function
 	| DirModule (dir,_) -> "Module", dir
 	| DirClosedSection dir -> "Closed Section", dir
       in
-      str s ++ spc () ++ pr_dirpath dir
+      str s ++ spc () ++ DirPath.print dir
   | ModuleType mp ->
       str "Module Type" ++ spc () ++ pr_path (Nametab.path_of_modtype mp)
   | Other (obj, info) -> info.name obj
@@ -647,7 +647,7 @@ let gallina_print_library_entry env sigma with_values ent =
     | (oname,Lib.ClosedSection _) ->
         Some (str " >>>>>>> Closed Section " ++ pr_name oname)
     | (_,Lib.CompilingLibrary (dir,_)) ->
-	Some (str " >>>>>>> Library " ++ pr_dirpath dir)
+        Some (str " >>>>>>> Library " ++ DirPath.print dir)
     | (oname,Lib.OpenedModule _) ->
 	Some (str " >>>>>>> Module " ++ pr_name oname)
     | (oname,Lib.ClosedModule _) ->
-- 
cgit v1.2.3