From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 kernel/byterun/coq_instruct.h | 4 ++++
 kernel/byterun/int64_emul.h   | 2 +-
 kernel/byterun/int64_native.h | 2 +-
 kernel/byterun/libcoqrun.clib | 4 ++++
 4 files changed, 10 insertions(+), 2 deletions(-)
 create mode 100644 kernel/byterun/libcoqrun.clib

(limited to 'kernel/byterun')

diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h
index 8a45e973..e224a108 100644
--- a/kernel/byterun/coq_instruct.h
+++ b/kernel/byterun/coq_instruct.h
@@ -11,6 +11,10 @@
 #ifndef _COQ_INSTRUCT_
 #define _COQ_INSTRUCT_
 
+/* Nota: this list of instructions is parsed to produce derived files */
+/* coq_jumptbl.h and copcodes.ml. Instructions should be uppercase    */
+/* and alone on lines starting by two spaces.                         */
+
 enum instructions {
   ACC0, ACC1, ACC2, ACC3, ACC4, ACC5, ACC6, ACC7, ACC,
   PUSH, 
diff --git a/kernel/byterun/int64_emul.h b/kernel/byterun/int64_emul.h
index 0a61ad79..04e38656 100644
--- a/kernel/byterun/int64_emul.h
+++ b/kernel/byterun/int64_emul.h
@@ -11,7 +11,7 @@
 /*                                                                     */
 /***********************************************************************/
 
-/* $Id: int64_emul.h 10739 2008-04-01 14:45:20Z herbelin $ */
+/* $Id$ */
 
 /* 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..f5bef4a6 100644
--- a/kernel/byterun/int64_native.h
+++ b/kernel/byterun/int64_native.h
@@ -11,7 +11,7 @@
 /*                                                                     */
 /***********************************************************************/
 
-/* $Id: int64_native.h 10739 2008-04-01 14:45:20Z herbelin $ */
+/* $Id$ */
 
 /* Wrapper macros around native 64-bit integer arithmetic,
    so that it has the same interface as the software emulation
diff --git a/kernel/byterun/libcoqrun.clib b/kernel/byterun/libcoqrun.clib
new file mode 100644
index 00000000..c06e4086
--- /dev/null
+++ b/kernel/byterun/libcoqrun.clib
@@ -0,0 +1,4 @@
+coq_fix_code.o
+coq_memory.o
+coq_values.o
+coq_interp.o
-- 
cgit v1.2.3