From d3eac3d5fc8e5af499eb8750ca08ead8562dac6f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sat, 28 Dec 2013 20:39:17 -0500
Subject: Removing native_name reference from constant_body.

For now, this reference (renamed to link_info) has been moved to the
environment (for constants and inductive types). But this is only a first step
towards making the native compiler more functional.
---
 kernel/nativelibrary.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel/nativelibrary.ml')

diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 55d3485503..39717c351c 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -24,7 +24,7 @@ let rec translate_mod prefix mp env mod_expr acc =
       List.fold_left (translate_field prefix mp env') acc struc
   | MoreFunctor _ -> acc
 
-and translate_field prefix mp env (code, upds as acc) (l,x) =
+and translate_field prefix mp env acc (l,x) =
   match x with
   | SFBconst cb ->
       let con = make_con mp empty_dirpath l in
@@ -45,13 +45,13 @@ let dump_library mp dp env mod_expr =
       let t0 = Sys.time () in
       clear_global_tbl ();
       clear_symb_tbl ();
-      let mlcode, upds =
-        List.fold_left (translate_field prefix mp env) ([],empty_updates) struc
+      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 (), upds
+      mlcode, get_symbols_tbl ()
   | _ -> assert false
 
 
-- 
cgit v1.2.3