diff options
| author | Guillaume Melquiond | 2020-03-09 15:15:44 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2020-03-09 15:15:44 +0100 |
| commit | 4666a8b9596f8cb87b63c345f6e57348f0bfda6d (patch) | |
| tree | 8859730145ab59400fd1cbd5055b72f876ec3d0b | |
| parent | a028a97005b88a66a9d6dbaa4f0ade38859beffb (diff) | |
Do not rely on the implicit declaration of caml_minor_collection.
This commit also prefixes young_ptr and young_limit along the way, so as
to not rely on OCaml's compatibility layer. This is a gratuitous change,
since this code is only meant to be compiled with OCaml < 4.10 anyway.
| -rw-r--r-- | kernel/byterun/coq_interp.c | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index c30648197f..7588c1ce07 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -30,18 +30,20 @@ #include "coq_float64.h" #if OCAML_VERSION < 41000 +extern void caml_minor_collection(void); + #undef Alloc_small #define Alloc_small(result, wosize, tag) do{ \ - young_ptr -= Bhsize_wosize (wosize); \ - if (young_ptr < young_limit){ \ - young_ptr += Bhsize_wosize (wosize); \ + caml_young_ptr -= Bhsize_wosize(wosize); \ + if (caml_young_ptr < caml_young_limit) { \ + caml_young_ptr += Bhsize_wosize(wosize); \ Setup_for_gc; \ - minor_collection (); \ + caml_minor_collection(); \ Restore_after_gc; \ - young_ptr -= Bhsize_wosize (wosize); \ + caml_young_ptr -= Bhsize_wosize(wosize); \ } \ - Hd_hp (young_ptr) = Make_header ((wosize), (tag), Caml_black); \ - (result) = Val_hp (young_ptr); \ + Hd_hp(caml_young_ptr) = Make_header((wosize), (tag), Caml_black); \ + (result) = Val_hp(caml_young_ptr); \ }while(0) #endif |