diff options
Diffstat (limited to 'vernac/ppvernac.ml')
| -rw-r--r-- | vernac/ppvernac.ml | 14 |
1 files changed, 5 insertions, 9 deletions
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 314c423f65..33d9e3d98a 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1016,22 +1016,18 @@ let string_of_definition_object_kind = let open Decls in function return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c) (* Auxiliary file and library management *) - | VernacAddLoadPath (fl,s,d) -> + | VernacAddLoadPath { implicit; physical_path; logical_path } -> return ( hov 2 (keyword "Add" ++ - (if fl then spc () ++ keyword "Rec" ++ spc () else spc()) ++ - keyword "LoadPath" ++ spc() ++ qs s ++ - (match d with - | None -> mt() - | Some dir -> spc() ++ keyword "as" ++ spc() ++ DirPath.print dir)) - ) + (if implicit then spc () ++ keyword "Rec" ++ spc () else spc()) ++ + keyword "LoadPath" ++ spc() ++ qs physical_path ++ + spc() ++ keyword "as" ++ spc() ++ DirPath.print logical_path)) | VernacRemoveLoadPath s -> return (keyword "Remove LoadPath" ++ qs s) - | VernacAddMLPath (fl,s) -> + | VernacAddMLPath (s) -> return ( keyword "Add" - ++ (if fl then spc () ++ keyword "Rec" ++ spc () else spc()) ++ keyword "ML Path" ++ qs s ) |