aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelibrary.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2015-07-18 12:18:05 +0200
committerPierre-Marie Pédrot2015-07-18 12:18:05 +0200
commit88e2da8c1b9403f5eac19df4f6c55fedca948bcc (patch)
tree01f750142359361f800e0dc2dfe422f145f491c5 /kernel/nativelibrary.ml
parent139c92bebd3f3d22c9f4d8220647bb7dd4e43890 (diff)
parentfdd6a17b272995237c9f95fc465bb1ff6871bedc (diff)
Merge branch 'v8.5'
Diffstat (limited to 'kernel/nativelibrary.ml')
-rw-r--r--kernel/nativelibrary.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 0b8662ff0b..443cd8c2a0 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -62,12 +62,12 @@ let dump_library mp dp env mod_expr =
let prefix = mod_uid_of_dirpath dp ^ "." in
let t0 = Sys.time () in
clear_global_tbl ();
- clear_symb_tbl ();
+ clear_symbols ();
let mlcode =
List.fold_left (translate_field prefix mp env) [] struc
in
let t1 = Sys.time () in
let time_info = Format.sprintf "Time spent generating this code: %.5fs" (t1-.t0) in
let mlcode = add_header_comment (List.rev mlcode) time_info in
- mlcode, get_symbols_tbl ()
+ mlcode, get_symbols ()
| _ -> assert false