diff options
| author | Maxime Dénès | 2013-12-28 20:39:17 -0500 |
|---|---|---|
| committer | Maxime Dénès | 2013-12-28 20:39:17 -0500 |
| commit | d3eac3d5fc8e5af499eb8750ca08ead8562dac6f (patch) | |
| tree | 70540c3d5e8b0856db2a9e82710e1b32cdc8465d /kernel/nativelibrary.ml | |
| parent | a681e57e3c76dff2fe710ce533179ea659d8de0b (diff) | |
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.
Diffstat (limited to 'kernel/nativelibrary.ml')
| -rw-r--r-- | kernel/nativelibrary.ml | 8 |
1 files changed, 4 insertions, 4 deletions
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 |
