Moving the VM global atom table to a ML reference.

1 files changed, 10 insertions, 6 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index ced2a175d0..cfeb0a9ee1 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -163,10 +163,10 @@ extern void caml_process_pending_signals(void);
 /* The interpreter itself */
 
 value coq_interprete
-(code_t coq_pc, value coq_accu, value coq_global_data, value coq_env, long coq_extra_args)
+(code_t coq_pc, value coq_accu, value coq_atom_tbl, value coq_global_data, value coq_env, long coq_extra_args)
 {
   /* coq_accu is not allocated on the OCaml heap */
-  CAMLparam1(coq_global_data);
+  CAMLparam2(coq_atom_tbl, coq_global_data);
 
   /*Declaration des variables */
 #ifdef PC_REG
@@ -1515,12 +1515,16 @@ value coq_push_vstack(value stk, value max_stack_size) {
   return Val_unit;
 }
 
-value  coq_interprete_ml(value tcode, value a, value g, value e, value ea) {
+value  coq_interprete_ml(value tcode, value a, value t, value g, value e, value ea) {
   print_instr("coq_interprete");
-  return coq_interprete((code_t)tcode, a, g, e, Long_val(ea));
+  return coq_interprete((code_t)tcode, a, t, g, e, Long_val(ea));
   print_instr("end coq_interprete");
 }
 
-value coq_eval_tcode (value tcode, value g, value e) {
-  return coq_interprete_ml(tcode, Val_unit, g, e, 0);
+value coq_interprete_byte(value* argv, int argn){
+  return coq_interprete_ml(argv[0], argv[1], argv[2], argv[3], argv[4], argv[5]);
+}
+
+value coq_eval_tcode (value tcode, value t, value g, value e) {
+  return coq_interprete_ml(tcode, Val_unit, t, g, e, 0);
 }