diff options
| author | Maxime Dénès | 2017-11-13 11:22:41 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-13 11:22:41 +0100 |
| commit | b75f803afb3189a9f3b594a190fdb8d6207e7624 (patch) | |
| tree | 28b33d0d1ffa2fbe42d044235987f34b0c733fbb /library/libnames.ml | |
| parent | a7df689e73dd396dafdbb4891d534b7fa5cb0fc8 (diff) | |
| parent | f3abbc55ef160d1a65d4467bfe9b25b30b965a46 (diff) | |
Merge PR #6065: [api] Deprecate all legacy uses of Names in core.
Diffstat (limited to 'library/libnames.ml')
| -rw-r--r-- | library/libnames.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/library/libnames.ml b/library/libnames.ml index 0453f15e87..efb1348ab2 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 |