From 8fa3c26adb1bc2c0201a61adede278a0e889eef4 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 23 Nov 2017 14:48:05 +0100 Subject: Move the call to the computation of bytecode inside Cemitcodes. This shouldn't matter because the tcode_of_code function is pure, its only effect being allocating a string and filling it with the translated bytecode. --- kernel/cemitcodes.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'kernel/cemitcodes.ml') diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index bc6140ef4..41494441b 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -15,6 +15,10 @@ open Cbytecodes open Copcodes open Mod_subst +type emitcodes = String.t + +external tcode_of_code : emitcodes -> int -> Vmvalues.tcode = "coq_tcode_of_code" + (* Relocation information *) type reloc_info = | Reloc_annot of annot_switch @@ -57,9 +61,10 @@ let patch_int buff patches = let patch buff pl f = let map (r, pos) = (pos, f r) in + (** Order seems important here? *) let patches = CList.map_left map pl in let buff = patch_int buff patches in - buff + tcode_of_code buff (String.length buff) (* Buffering of bytecode *) @@ -327,10 +332,6 @@ let init () = label_table := Array.make 16 (Label_undefined []); reloc_info := [] -type emitcodes = String.t - -let length = String.length - type to_patch = emitcodes * (patch list) * fv (* Substitution *) -- cgit v1.2.3