From 6acf543800fe176ca7d47ef7165ebc14588efb6f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 29 Apr 2014 14:41:49 -0400
Subject: Native compiler: hide compiled files in a .coq-native subdirectory.

---
 kernel/nativelibrary.ml | 7 -------
 1 file changed, 7 deletions(-)

(limited to 'kernel/nativelibrary.ml')

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)
-- 
cgit v1.2.3