diff options
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 : |