From f3abbc55ef160d1a65d4467bfe9b25b30b965a46 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 4 Nov 2017 18:58:27 +0100
Subject: [api] Deprecate all legacy uses of Names in core.

This will allow to merge back `Names` with `API.Names`
---
 kernel/nativelib.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/nativelib.mli')

diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli
index a262a9f58a..b74d4fdd05 100644
--- a/kernel/nativelib.mli
+++ b/kernel/nativelib.mli
@@ -21,7 +21,7 @@ val get_ml_filename : unit -> string * string
 
 val compile : string -> global list -> profile:bool -> bool * string
 
-val compile_library : Names.dir_path -> global list -> string -> bool
+val compile_library : Names.DirPath.t -> global list -> string -> bool
 
 val call_linker :
   ?fatal:bool -> string -> string -> code_location_updates option -> unit
-- 
cgit v1.2.3