aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/libnames.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/libnames.ml')
-rw-r--r--library/libnames.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/library/libnames.ml b/library/libnames.ml
index 0453f15e8..efb1348ab 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -154,12 +154,12 @@ let qualid_of_dirpath dir =
let (l,a) = split_dirpath dir in
make_qualid l a
-type object_name = full_path * kernel_name
+type object_name = full_path * KerName.t
-type object_prefix = DirPath.t * (module_path * DirPath.t)
+type object_prefix = DirPath.t * (ModPath.t * DirPath.t)
let make_oname (dirpath,(mp,dir)) id =
- make_path dirpath id, make_kn mp dir (Label.of_id id)
+ make_path dirpath id, KerName.make mp dir (Label.of_id id)
(* to this type are mapped DirPath.t's in the nametab *)
type global_dir_reference =
@@ -173,7 +173,7 @@ type global_dir_reference =
let eq_op (d1, (mp1, p1)) (d2, (mp2, p2)) =
DirPath.equal d1 d2 &&
DirPath.equal p1 p2 &&
- mp_eq mp1 mp2
+ ModPath.equal mp1 mp2
let eq_global_dir_reference r1 r2 = match r1, r2 with
| DirOpenModule op1, DirOpenModule op2 -> eq_op op1 op2