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