From 8af91e636038cb113bbd16f7f8225196190bb2d4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 16 Apr 2019 19:56:38 +0200
Subject: [doc] [kernel] Add docstrings for native interface functions.

---
 kernel/nativelib.mli | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'kernel/nativelib.mli')

diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli
index d8557e667f..e113350368 100644
--- a/kernel/nativelib.mli
+++ b/kernel/nativelib.mli
@@ -21,8 +21,13 @@ val load_obj : (string -> unit) ref
 
 val get_ml_filename : unit -> string * string
 
+(** [compile file code ~profile] will compile native [code] to [file],
+   and return the name of the object file; this name depends on
+   whether are in byte mode or not; file is expected to be .ml file *)
 val compile : string -> global list -> profile:bool -> string
 
+(** [compile_library lib code file] is similar to [compile file code]
+   but will perform some extra tweaks to handle [code] as a Coq lib. *)
 val compile_library : Names.DirPath.t -> global list -> string -> unit
 
 val call_linker :
-- 
cgit v1.2.3