diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 15:57:08 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 15:57:08 +0000 |
| commit | f42dd8d8530e6227621ccd662741f1da23700304 (patch) | |
| tree | 1838306cdafaa8486ec792c1ab48b64162e027c9 /pretyping | |
| 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 'pretyping')
| -rw-r--r-- | pretyping/namegen.ml | 2 | ||||
| -rw-r--r-- | pretyping/program.ml | 2 | ||||
| -rw-r--r-- | pretyping/termops.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index 5e725979b..a7b49fbe2 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_eq dp1 dp) + |MPfile dp1 -> not (Dir_path.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 a0befa130..d2e22f71e 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -11,7 +11,7 @@ open Util open Names open Term -let make_dir l = make_dirpath (List.map Id.of_string (List.rev l)) +let make_dir l = Dir_path.make (List.map Id.of_string (List.rev l)) let find_reference locstr dir s = let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 2cc538004..f48734be7 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 empty_dirpath +(*let current_module = ref Dir_path.empty let set_module m = current_module := m*) |