aboutsummaryrefslogtreecommitdiff
path: root/kernel/byterun
diff options
context:
space:
mode:
authorPierre Boutillier2015-06-22 11:49:58 +0200
committerPierre Boutillier2015-06-22 11:49:58 +0200
commit6bec099f8487b9d3ec5c44079cf69d3474c73b91 (patch)
treeb23d8983fa887cc7e7255df455c64d5d54130787 /kernel/byterun
parent07e8eede6670a256a81d9d70133ebbeb64f45fe3 (diff)
parent949d027ce8fa94b5c62f938b58c3f85d015b177b (diff)
Merge remote-tracking branch 'forge/v8.5'
Diffstat (limited to 'kernel/byterun')
-rw-r--r--kernel/byterun/coq_gc.h13
1 files changed, 12 insertions, 1 deletions
diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h
index c7b18b9006..f06275862c 100644
--- a/kernel/byterun/coq_gc.h
+++ b/kernel/byterun/coq_gc.h
@@ -12,6 +12,7 @@
#define _COQ_CAML_GC_
#include <caml/mlvalues.h>
#include <caml/alloc.h>
+#include <caml/memory.h>
typedef void (*scanning_action) (value, value *);
@@ -24,12 +25,22 @@ CAMLextern void minor_collection (void);
#define Caml_white (0 << 8)
#define Caml_black (3 << 8)
+#ifdef HAS_OCP_MEMPROF
+
+/* This code is necessary to make the OCamlPro memory profiling branch of
+ OCaml compile. */
+
+#define Make_header(wosize, tag, color) \
+ caml_make_header(wosize, tag, color)
+
+#else
+
#define Make_header(wosize, tag, color) \
(((header_t) (((header_t) (wosize) << 10) \
+ (color) \
+ (tag_t) (tag))) \
)
-
+#endif
#define Alloc_small(result, wosize, tag) do{ \
young_ptr -= Bhsize_wosize (wosize); \