From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 kernel/byterun/coq_interp.c   | 21 +++++++--------------
 kernel/byterun/coq_memory.c   |  6 ------
 kernel/byterun/coq_memory.h   |  1 -
 kernel/byterun/int64_emul.h   |  2 --
 kernel/byterun/int64_native.h |  2 --
 5 files changed, 7 insertions(+), 25 deletions(-)

(limited to 'kernel/byterun')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index a0cb4f1a..aab08d89 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -81,13 +81,6 @@ sp is a local copy of the global variable extern_sp. */
 #   define print_int(i) 
 #endif
 
-/* Wrapper pour caml_modify */ 	 
-#ifdef OCAML_307 	 
-#define CAML_MODIFY(a,b) modify(a,b) 	 
-#else 	 
-#define CAML_MODIFY(a,b) caml_modify(a,b) 	 
-#endif
-
 /* GC interface */
 #define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; }
 #define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; }
@@ -158,7 +151,7 @@ sp is a local copy of the global variable extern_sp. */
 #endif
 #endif
 
-/* For signal handling, we highjack some code from the caml runtime */
+/* For signal handling, we hijack some code from the caml runtime */
 
 extern intnat caml_signals_are_pending;
 extern intnat caml_pending_signals[];
@@ -671,7 +664,7 @@ value coq_interprete
 	  Field(accu, 0) = sp[0];
 	  *sp = accu;
 	  /* mise a jour du block accumulate */
-	  CAML_MODIFY(&Field(p[i], 1),*sp);
+	  caml_modify(&Field(p[i], 1),*sp);
 	  sp++;
 	}
 	pc += nfunc;
@@ -842,7 +835,7 @@ value coq_interprete
       
       Instruct(SETFIELD0){
 	print_instr("SETFIELD0");
-	CAML_MODIFY(&Field(accu, 0),*sp);
+	caml_modify(&Field(accu, 0),*sp);
 	sp++;
 	Next;
       }
@@ -850,7 +843,7 @@ value coq_interprete
       Instruct(SETFIELD1){
         int i, j, size, size_aux;
 	print_instr("SETFIELD1");
-	CAML_MODIFY(&Field(accu, 1),*sp);
+	caml_modify(&Field(accu, 1),*sp);
        	sp++;
 	Next; 
       }
@@ -868,9 +861,9 @@ value coq_interprete
 	    *sp = accu;
 	    Alloc_small(accu, 1, ATOM_COFIX_TAG);
 	    Field(accu, 0) = Field(Field(*sp, 1), 0);
-	    CAML_MODIFY(&Field(*sp, 1), accu);
+	    caml_modify(&Field(*sp, 1), accu);
 	    accu = *sp; sp++;
-            CAML_MODIFY(&Field(*sp, i), accu);
+            caml_modify(&Field(*sp, i), accu);
 	  }
 	}
 	sp++;
@@ -879,7 +872,7 @@ value coq_interprete
       
       Instruct(SETFIELD){
 	print_instr("SETFIELD");
-	CAML_MODIFY(&Field(accu, *pc),*sp);
+	caml_modify(&Field(accu, *pc),*sp);
 	sp++; pc++;
 	Next;
       }	
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 91342108..00f5eb3b 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -50,12 +50,6 @@ value coq_static_alloc(value size) /* ML */
   return (value) coq_stat_alloc((asize_t) Long_val(size));
 }
 
-value coq_static_free(value blk)  /* ML */
-{
-  coq_stat_free((void *) blk);
-  return Val_unit;
-}
-
 value accumulate_code(value unit) /* ML */
 {
   return (value) accumulate;
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
index c0093a49..79e4d0fe 100644
--- a/kernel/byterun/coq_memory.h
+++ b/kernel/byterun/coq_memory.h
@@ -49,7 +49,6 @@ extern code_t accumulate;
 /* functions over global environment */
 
 value coq_static_alloc(value size);  /* ML */
-value coq_static_free(value string); /* ML */
 
 value init_coq_vm(value unit); /* ML */
 value re_init_coq_vm(value unit); /* ML */
diff --git a/kernel/byterun/int64_emul.h b/kernel/byterun/int64_emul.h
index 0a61ad79..86bee72e 100644
--- a/kernel/byterun/int64_emul.h
+++ b/kernel/byterun/int64_emul.h
@@ -11,8 +11,6 @@
 /*                                                                     */
 /***********************************************************************/
 
-/* $Id: int64_emul.h 10739 2008-04-01 14:45:20Z herbelin $ */
-
 /* Software emulation of 64-bit integer arithmetic, for C compilers
    that do not support it.  */
 
diff --git a/kernel/byterun/int64_native.h b/kernel/byterun/int64_native.h
index 4fc3c220..8a6a2664 100644
--- a/kernel/byterun/int64_native.h
+++ b/kernel/byterun/int64_native.h
@@ -11,8 +11,6 @@
 /*                                                                     */
 /***********************************************************************/
 
-/* $Id: int64_native.h 10739 2008-04-01 14:45:20Z herbelin $ */
-
 /* Wrapper macros around native 64-bit integer arithmetic,
    so that it has the same interface as the software emulation
    provided in int64_emul.h */
-- 
cgit v1.2.3