diff options
Diffstat (limited to 'library/libnames.ml')
| -rw-r--r-- | library/libnames.ml | 31 |
1 files changed, 0 insertions, 31 deletions
diff --git a/library/libnames.ml b/library/libnames.ml index bd2ca550b9..87c4de42e8 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -162,37 +162,6 @@ 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 - | DirOpenModtype of object_prefix - | DirOpenSection of object_prefix - | DirModule of object_prefix - -let eq_op op1 op2 = - DirPath.equal op1.obj_dir op2.obj_dir && - DirPath.equal op1.obj_sec op2.obj_sec && - ModPath.equal op1.obj_mp op2.obj_mp - -let eq_global_dir_reference r1 r2 = match r1, r2 with -| DirOpenModule op1, DirOpenModule op2 -> eq_op op1 op2 -| DirOpenModtype op1, DirOpenModtype op2 -> eq_op op1 op2 -| DirOpenSection op1, DirOpenSection op2 -> eq_op op1 op2 -| DirModule op1, DirModule op2 -> eq_op op1 op2 -| _ -> false - (* Default paths *) let default_library = Names.DirPath.initial (* = ["Top"] *) |