aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/byterun
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/byterun')
-rw-r--r--kernel/byterun/coq_interp.c15
1 files changed, 11 insertions, 4 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index ccfb2515a..0dd3b653a 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -80,6 +80,13 @@ sp is a local copy of the global variable extern_sp. */
# define print_int(i)
#endif
+/* Wrapper pour caml_modify */
+#ifdef OCAML_307
+#define CAML_MODIFY(a,b) modify(a,b)
+#else
+#define CAML_MODIFY(a,b) caml_modify(a,b)
+#endif
+
/* GC interface */
#define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; }
#define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; }
@@ -652,7 +659,7 @@ value coq_interprete
Field(accu, 0) = sp[0];
*sp = accu;
/* mise a jour du block accumulate */
- caml_modify(&Field(p[i], 1),*sp);
+ CAML_MODIFY(&Field(p[i], 1),*sp);
sp++;
}
pc += nfunc;
@@ -823,7 +830,7 @@ value coq_interprete
Instruct(SETFIELD0){
print_instr("SETFIELD0");
- caml_modify(&Field(accu, 0),*sp);
+ CAML_MODIFY(&Field(accu, 0),*sp);
sp++;
Next;
}
@@ -831,7 +838,7 @@ value coq_interprete
Instruct(SETFIELD1){
int i, j, size, size_aux;
print_instr("SETFIELD1");
- caml_modify(&Field(accu, 1),*sp);
+ CAML_MODIFY(&Field(accu, 1),*sp);
sp++;
Next;
}
@@ -860,7 +867,7 @@ value coq_interprete
Instruct(SETFIELD){
print_instr("SETFIELD");
- caml_modify(&Field(accu, *pc),*sp);
+ CAML_MODIFY(&Field(accu, *pc),*sp);
sp++; pc++;
Next;
}