diff options
Diffstat (limited to 'library/libnames.ml')
| -rw-r--r-- | library/libnames.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/library/libnames.ml b/library/libnames.ml index bd2ca550b9..f6fc5ed4b7 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -162,18 +162,12 @@ let qualid_basename qid = let qualid_path qid = qid.CAst.v.dirpath -type object_name = full_path * KerName.t - type object_prefix = { obj_dir : DirPath.t; obj_mp : ModPath.t; obj_sec : DirPath.t; } -(* let make_oname (dirpath,(mp,dir)) id = *) -let make_oname { obj_dir; obj_mp } id = - make_path obj_dir id, KerName.make obj_mp (Label.of_id id) - (* to this type are mapped DirPath.t's in the nametab *) type global_dir_reference = | DirOpenModule of object_prefix |