diff options
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*) |