From 55ce117e8083477593cf1ff2e51a3641c7973830 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 13 Feb 2007 13:48:12 +0000
Subject: Imported Upstream version 8.1+dfsg

---
 kernel/byterun/coq_fix_code.c | 10 +++++-----
 kernel/byterun/coq_fix_code.h |  2 +-
 kernel/byterun/coq_gc.h       |  4 ++--
 kernel/byterun/coq_interp.c   |  6 +-----
 kernel/byterun/coq_interp.h   |  4 ++++
 kernel/byterun/coq_memory.c   |  7 +------
 kernel/byterun/coq_memory.h   | 10 +++++-----
 kernel/byterun/coq_values.c   |  2 +-
 kernel/byterun/coq_values.h   |  4 ++--
 9 files changed, 22 insertions(+), 27 deletions(-)

(limited to 'kernel/byterun')

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 70648b44..affcccb3 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -10,11 +10,11 @@
 
 #include <stdio.h>
 #include <stdlib.h> 
-#include "config.h"
-#include "misc.h"
-#include "mlvalues.h"
-#include "fail.h"
-#include "memory.h"
+#include <config.h>
+#include <misc.h>
+#include <mlvalues.h>
+#include <fail.h>
+#include <memory.h>
 #include "coq_instruct.h"
 #include "coq_fix_code.h"
 
diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h
index 035d5b9b..d1dac80f 100644
--- a/kernel/byterun/coq_fix_code.h
+++ b/kernel/byterun/coq_fix_code.h
@@ -12,7 +12,7 @@
 #ifndef _COQ_FIX_CODE_
 #define _COQ_FIX_CODE_
 
-#include "mlvalues.h"
+#include <mlvalues.h>
 void * coq_stat_alloc (asize_t sz);
 
 #ifdef THREADED_CODE
diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h
index 2f085326..ccccbe78 100644
--- a/kernel/byterun/coq_gc.h
+++ b/kernel/byterun/coq_gc.h
@@ -10,8 +10,8 @@
 
 #ifndef _COQ_CAML_GC_
 #define _COQ_CAML_GC_
-#include "mlvalues.h"
-#include "alloc.h"
+#include <mlvalues.h>
+#include <alloc.h>
 
 typedef void (*scanning_action) (value, value *);
 
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 0f91a7e3..8f9c10e6 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -44,11 +44,7 @@ sp is a local copy of the global variable extern_sp. */
 #  ifdef DEBUG
 #    define Next goto next_instr
 #  else
-#    ifdef __ia64__
-#      define Next goto *(void *)(coq_jumptbl_base + *((uint32 *) pc)++)
-#    else
-#      define Next goto *(void *)(coq_jumptbl_base + *pc++)
-#    endif
+#    define Next goto *(void *)(coq_jumptbl_base + *pc++)  
 #  endif
 #else 
 #  define Instruct(name) case name:
diff --git a/kernel/byterun/coq_interp.h b/kernel/byterun/coq_interp.h
index 76e68944..60865c32 100644
--- a/kernel/byterun/coq_interp.h
+++ b/kernel/byterun/coq_interp.h
@@ -19,5 +19,9 @@ value coq_push_vstack(value stk);
 
 value  coq_interprete_ml(value tcode, value a, value e, value ea);
 
+value coq_interprete
+    (code_t coq_pc, value coq_accu, value coq_env, long coq_extra_args);
+
 value coq_eval_tcode (value tcode, value e);
 
+
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;
-}
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
index 0d866dc7..edd05948 100644
--- a/kernel/byterun/coq_memory.h
+++ b/kernel/byterun/coq_memory.h
@@ -11,11 +11,11 @@
 #ifndef _COQ_MEMORY_
 #define _COQ_MEMORY_
 
-#include "config.h"
-#include "fail.h"
-#include "misc.h"
-#include "memory.h"
-#include "mlvalues.h"
+#include <config.h>
+#include <fail.h>
+#include <misc.h>
+#include <memory.h>
+#include <mlvalues.h>
 
 
 #define Coq_stack_size (4096 * sizeof(value))
diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c
index 34b885e8..007f61b2 100644
--- a/kernel/byterun/coq_values.c
+++ b/kernel/byterun/coq_values.c
@@ -13,7 +13,7 @@
 #include "coq_instruct.h"
 #include "coq_memory.h"
 #include "coq_values.h"
-#include "memory.h"
+#include <memory.h>
 /* KIND OF VALUES */
 
 #define Setup_for_gc
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index a5176f3f..4c631fce 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -11,8 +11,8 @@
 #ifndef _COQ_VALUES_
 #define _COQ_VALUES_
 
-#include "alloc.h"
-#include "mlvalues.h"
+#include <alloc.h>
+#include <mlvalues.h>
 
 #define Default_tag 0
 #define Accu_tag 0
-- 
cgit v1.2.3