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 ++++++-----
 kernel/cemitcodes.mli |  4 +---
 kernel/csymtable.ml   |  4 +---
 3 files changed, 8 insertions(+), 11 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index bc6140ef45..41494441b4 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 *)
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index a2ff2d3019..aa055dcb02 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -9,9 +9,7 @@ type reloc_info =
 type patches
 type emitcodes
 
-val length : emitcodes -> int
-
-val patch : emitcodes -> patches -> (reloc_info -> int) -> emitcodes
+val patch : emitcodes -> patches -> (reloc_info -> int) -> Vmvalues.tcode
 
 type to_patch = emitcodes * patches * fv
 
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 38044071f0..8022eae7dd 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -25,7 +25,6 @@ open Cbytegen
 module NamedDecl = Context.Named.Declaration
 module RelDecl = Context.Rel.Declaration
 
-external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code"
 external eval_tcode : tcode -> values array -> values = "coq_eval_tcode"
 
 (*******************)
@@ -210,9 +209,8 @@ and eval_to_patch env (buff,pl,fv) =
     | Reloc_const sc -> slot_for_str_cst sc
     | Reloc_getglobal kn -> slot_for_getglobal env kn
   in
-  let buff = patch buff pl slots in
+  let tc = patch buff pl slots in
   let vm_env = Array.map (slot_for_fv env) fv in
-  let tc = tcode_of_code buff (length buff) in
   eval_tcode tc vm_env
 
 and val_of_constr env c =
-- 
cgit v1.2.3