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/nativelibrary.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/nativelibrary.mli') diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli index f327ba224..72e3d8041 100644 --- a/kernel/nativelibrary.mli +++ b/kernel/nativelibrary.mli @@ -13,5 +13,5 @@ open Nativecode (** This file implements separate compilation for libraries in the native compiler *) -val dump_library : module_path -> dir_path -> env -> module_signature -> +val dump_library : ModPath.t -> DirPath.t -> env -> module_signature -> global list * symbols -- cgit v1.2.3