diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 07:42:16 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-21 23:26:19 +0100 |
| commit | 23f0f5fe6b510d2ab91a2917eb895faa479d9fcf (patch) | |
| tree | 73ce61804aae0e16b1a30994affd75a59ed08efe /printing | |
| parent | eb91ccaf236bc9a60a1e216b76a0a42980c072a7 (diff) | |
[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.
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 _) -> |