aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-06-01 13:39:16 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-06-01 14:39:12 +0200
commit3b917b7b9a201b511a56f55102077199868212e7 (patch)
treefe97c1a26e2c7508f52d0e4ca118841e8e99fee9
parent43aa642ad4f2d30029c1c1f272ba162b6801a40b (diff)
Making Coq compile with ocp-memprof.
Patch provided by Çagdas Bozman.
-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 c7b18b900..f06275862 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); \