diff options
| author | Maxime Dénès | 2014-04-29 14:41:49 -0400 |
|---|---|---|
| committer | Maxime Dénès | 2014-04-29 14:41:49 -0400 |
| commit | 6acf543800fe176ca7d47ef7165ebc14588efb6f (patch) | |
| tree | 1bf524ee47195cc4d3ebdd48113aaeeaf1bc5c1d /kernel/nativelibrary.ml | |
| parent | 3b176883b7fcd9af6881ae1049bbd078c8d19577 (diff) | |
Native compiler: hide compiled files in a .coq-native subdirectory.
Diffstat (limited to 'kernel/nativelibrary.ml')
| -rw-r--r-- | kernel/nativelibrary.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index 6749dbfdba..f33e1eaa64 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -72,10 +72,3 @@ let dump_library mp dp env mod_expr = let mlcode = add_header_comment (List.rev mlcode) time_info in mlcode, get_symbols_tbl () | _ -> assert false - - -let compile_library dir code load_path f = - let header = mk_library_header dir in - let ml_filename = f^".native" in - write_ml_code ml_filename ~header code; - fst (call_compiler ml_filename load_path) |