aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-09-15 10:35:59 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-09-15 10:35:59 +0000
commitda3edaa7eab2bed17cdfb2c455f2e6b5b0318c4d (patch)
tree14b6ae25300dc08c9ca5ff86ad88a78910df7b92 /kernel
parent4f39e160d05b0e5501a909b3041589303651670b (diff)
* Adding compability with ocaml 3.10 + camlp5 (rework of
the patch by S. Mimram) * for detecting architecture, also look for /bin/uname * restore the compatibility of kernel/byterun/coq_interp.c with ocaml 3.07 (caml_modify vs. modify). There is still an issue with this 3.07 and 64-bits architecture (see coqdev and a future bug report). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10122 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
-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;
}