diff options
Diffstat (limited to 'intf/vernacexpr.mli')
| -rw-r--r-- | intf/vernacexpr.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 16175be0d..8088ba92a 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -38,11 +38,11 @@ type printable = | PrintSectionContext of reference | PrintInspect of int | PrintGrammar of string - | PrintLoadPath of dir_path option + | PrintLoadPath of Dir_path.t option | PrintModules | PrintModule of reference | PrintModuleType of reference - | PrintNamespace of dir_path + | PrintNamespace of Dir_path.t | PrintMLLoadPath | PrintMLModules | PrintName of reference or_by_notation @@ -290,7 +290,7 @@ type vernac_expr = (* Auxiliary file and library management *) | VernacRequireFrom of export_flag option * string - | VernacAddLoadPath of rec_flag * string * dir_path option + | VernacAddLoadPath of rec_flag * string * Dir_path.t option | VernacRemoveLoadPath of string | VernacAddMLPath of rec_flag * string | VernacDeclareMLModule of locality_flag * string list |