From c408e819ce39b27f0842c84b1b24c585ac5b6086 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 22 Mar 2017 01:14:50 +0100
Subject: [lib] [api] Introduce record for `object_prefix`

This is a minor cleanup adding a record in a try to structure the
state living in `Lib`.
---
 API/API.mli | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index 7ec3cbee3b..4c1dbeabce 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2070,7 +2070,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
-- 
cgit v1.2.3