diff options
| author | ppedrot | 2012-12-14 15:57:08 +0000 |
|---|---|---|
| committer | ppedrot | 2012-12-14 15:57:08 +0000 |
| commit | f42dd8d8530e6227621ccd662741f1da23700304 (patch) | |
| tree | 1838306cdafaa8486ec792c1ab48b64162e027c9 /intf | |
| parent | 67f5c70a480c95cfb819fc68439781b5e5e95794 (diff) | |
Modulification of dir_path
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 2 | ||||
| -rw-r--r-- | intf/vernacexpr.mli | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 26ab4b6667..08063cf2ae 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -167,7 +167,7 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr = (* For syntax extensions *) | TacAlias of Loc.t * string * - (Id.t * 'lev generic_argument) list * (dir_path * glob_tactic_expr) + (Id.t * 'lev generic_argument) list * (Dir_path.t * glob_tactic_expr) (** Possible arguments of a tactic definition *) diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 16175be0d0..8088ba92a9 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 |