summaryrefslogtreecommitdiff
path: root/kernel/byterun/coq_memory.c
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2007-02-13 13:48:12 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2007-02-13 13:48:12 +0000
commit55ce117e8083477593cf1ff2e51a3641c7973830 (patch)
treea82defb4105f175c71b0d13cae42831ce608c4d6 /kernel/byterun/coq_memory.c
parent208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff)
Imported Upstream version 8.1+dfsgupstream/8.1+dfsg
Diffstat (limited to 'kernel/byterun/coq_memory.c')
-rw-r--r--kernel/byterun/coq_memory.c7
1 files changed, 1 insertions, 6 deletions
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index bfcb6812..91342108 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -14,6 +14,7 @@
#include "coq_instruct.h"
#include "coq_fix_code.h"
#include "coq_memory.h"
+#include "coq_interp.h"
/* stack */
@@ -264,9 +265,3 @@ value coq_set_drawinstr(value unit)
return Val_unit;
}
-
-value coq_print_pointer(value p)
-{
- printf("pointer = %X\n", p);
- return Val_unit;
-}