diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2014-04-29 14:41:49 -0400 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-04-29 14:41:49 -0400 |
| commit | 6acf543800fe176ca7d47ef7165ebc14588efb6f (patch) | |
| tree | 1bf524ee47195cc4d3ebdd48113aaeeaf1bc5c1d /kernel/nativelibrary.mli | |
| parent | 3b176883b7fcd9af6881ae1049bbd078c8d19577 (diff) | |
Native compiler: hide compiled files in a .coq-native subdirectory.
Diffstat (limited to 'kernel/nativelibrary.mli')
| -rw-r--r-- | kernel/nativelibrary.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli index a45402a43..1de26b72c 100644 --- a/kernel/nativelibrary.mli +++ b/kernel/nativelibrary.mli @@ -15,6 +15,3 @@ compiler *) val dump_library : module_path -> dir_path -> env -> module_signature -> global list * symbol array - -val compile_library : - dir_path -> global list -> string list -> string -> int |