diff options
| author | notin | 2006-07-28 18:05:39 +0000 |
|---|---|---|
| committer | notin | 2006-07-28 18:05:39 +0000 |
| commit | 7e13b8a0627c09a49487dc64210fa4616cffc66c (patch) | |
| tree | b44dee28523fd5f63edde51c15571d69251ab221 /kernel/byterun | |
| parent | 5ce1ece6393b33a213dfba2e3b63a130e398d84f (diff) | |
Modifications dans les scripts de configuration (coqtop et coqide affichent maintenant le numéro de révision svn) + correction problème OCaml 3.07 et caml_;odify
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9063 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/byterun')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 180e2b011f..ab63ff23a9 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -65,6 +65,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) caml_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; } @@ -637,7 +644,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; @@ -808,21 +815,21 @@ value coq_interprete Instruct(SETFIELD0){ print_instr("SETFIELD0"); - caml_modify(&Field(accu, 0),*sp); + CAML_MODIFY(&Field(accu, 0),*sp); sp++; Next; } Instruct(SETFIELD1){ print_instr("SETFIELD1"); - caml_modify(&Field(accu, 1),*sp); + CAML_MODIFY(&Field(accu, 1),*sp); sp++; Next; } Instruct(SETFIELD){ print_instr("SETFIELD"); - caml_modify(&Field(accu, *pc),*sp); + CAML_MODIFY(&Field(accu, *pc),*sp); sp++; pc++; Next; } |