aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/lib.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/lib.ml')
-rw-r--r--library/lib.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/library/lib.ml b/library/lib.ml
index 9ac9b7c71..0f2f480cb 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -658,13 +658,13 @@ let rec split_mp mp =
| Names.MPdot (prfx, lbl) ->
let mprec, dprec = split_mp prfx in
mprec, Names.Dir_path.make (Names.Id.of_string (Names.Label.to_string lbl) :: (Names.Dir_path.repr dprec))
- | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in library_dp(), Names.Dir_path.make [id]
+ | Names.MPbound mbid -> let (_, id, dp) = Names.MBId.repr mbid in library_dp(), Names.Dir_path.make [id]
let split_modpath mp =
let rec aux = function
| Names.MPfile dp -> dp, []
| Names.MPbound mbid ->
- library_dp (), [Names.id_of_mbid mbid]
+ library_dp (), [Names.MBId.to_id mbid]
| Names.MPdot (mp,l) -> let (mp', lab) = aux mp in
(mp', Names.Label.to_id l :: lab)
in