diff options
| author | letouzey | 2013-02-19 20:27:51 +0000 |
|---|---|---|
| committer | letouzey | 2013-02-19 20:27:51 +0000 |
| commit | 248728628f5da946f96c22ba0a0e7e9b33019382 (patch) | |
| tree | 905dbbafa65dd7bf02823318326be2ca389f833f /intf | |
| parent | 3889c9a9e7d017ef2eea647d8c17d153a0b90083 (diff) | |
Dir_path --> DirPath
Ok, this is merely a matter of taste, but up to now the usage
in Coq is rather to use capital letters instead of _ in the
names of inner modules.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 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 1d7e9374f5..719cf0d33b 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.t * glob_tactic_expr) + (Id.t * 'lev generic_argument) list * (DirPath.t * glob_tactic_expr) (** Possible arguments of a tactic definition *) diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 528fd69f30..4655e3588d 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.t option + | PrintLoadPath of DirPath.t option | PrintModules | PrintModule of reference | PrintModuleType of reference - | PrintNamespace of Dir_path.t + | PrintNamespace of DirPath.t | PrintMLLoadPath | PrintMLModules | PrintName of reference or_by_notation @@ -289,7 +289,7 @@ type vernac_expr = (* Auxiliary file and library management *) | VernacRequireFrom of export_flag option * string - | VernacAddLoadPath of rec_flag * string * Dir_path.t option + | VernacAddLoadPath of rec_flag * string * DirPath.t option | VernacRemoveLoadPath of string | VernacAddMLPath of rec_flag * string | VernacDeclareMLModule of locality_flag * string list |