diff options
Diffstat (limited to 'kernel/cemitcodes.ml')
| -rw-r--r-- | kernel/cemitcodes.ml | 11 |
1 files changed, 6 insertions, 5 deletions
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 *) |