diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-19 20:27:51 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-19 20:27:51 +0000 |
| commit | 248728628f5da946f96c22ba0a0e7e9b33019382 (patch) | |
| tree | 905dbbafa65dd7bf02823318326be2ca389f833f /pretyping | |
| 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 'pretyping')
| -rw-r--r-- | pretyping/namegen.ml | 2 | ||||
| -rw-r--r-- | pretyping/program.ml | 2 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 2 | ||||
| -rw-r--r-- | pretyping/termops.ml | 2 |
4 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index 8009524de..bf1adb3cf 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -30,7 +30,7 @@ let is_imported_modpath mp = match mp with | MPfile dp -> let rec find_prefix = function - |MPfile dp1 -> not (Dir_path.equal dp1 dp) + |MPfile dp1 -> not (DirPath.equal dp1 dp) |MPdot(mp,_) -> find_prefix mp |MPbound(_) -> false in find_prefix current_mp diff --git a/pretyping/program.ml b/pretyping/program.ml index 1201ff8e0..a701fdef4 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -12,7 +12,7 @@ open Util open Names open Term -let make_dir l = Dir_path.make (List.rev_map Id.of_string l) +let make_dir l = DirPath.make (List.rev_map Id.of_string l) let find_reference locstr dir s = let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 7359b2e2a..624645a8f 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -259,7 +259,7 @@ let magicaly_constant_of_fixbody env bd = function | Name.Name id -> try let cst = Nametab.locate_constant - (Libnames.make_qualid Dir_path.empty id) in + (Libnames.make_qualid DirPath.empty id) in match constant_opt_value env cst with | None -> bd | Some t -> if eq_constr t bd then mkConst cst else bd diff --git a/pretyping/termops.ml b/pretyping/termops.ml index d10289820..825a6adb7 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -141,7 +141,7 @@ let print_env env = in (sign_env ++ db_env) -(*let current_module = ref Dir_path.empty +(*let current_module = ref DirPath.empty let set_module m = current_module := m*) |