diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 6 | ||||
| -rw-r--r-- | printing/prettyp.ml | 4 |
2 files changed, 5 insertions, 5 deletions
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 _) -> |