diff options
| author | Emilio Jesus Gallego Arias | 2019-04-16 19:56:38 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-16 19:56:38 +0200 |
| commit | 8af91e636038cb113bbd16f7f8225196190bb2d4 (patch) | |
| tree | 44c7beb990b1734704db3680dc2e87b10c5bd664 /kernel/nativelib.mli | |
| parent | 3c785936a0b56623f7c3512fa861a7a9823ad495 (diff) | |
[doc] [kernel] Add docstrings for native interface functions.
Diffstat (limited to 'kernel/nativelib.mli')
| -rw-r--r-- | kernel/nativelib.mli | 5 |
1 files changed, 5 insertions, 0 deletions
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 : |