Merge PR #6244: [lib] [api] Introduce record for `object_prefix`

1 files changed, 5 insertions, 1 deletions

diff --git a/API/API.mli b/API/API.mli
index 2eb7c4736e..b3efb3440f 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2077,7 +2077,11 @@ sig
   val basename : full_path -> Names.Id.t
 
   type object_name = full_path * Names.KerName.t
-  type object_prefix = Names.DirPath.t * (Names.ModPath.t * Names.DirPath.t)
+  type object_prefix = {
+    obj_dir : DirPath.t;
+    obj_mp  : ModPath.t;
+    obj_sec : DirPath.t;
+  }
 
   module Dirset : Set.S with type elt = DirPath.t
   module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset