diff options
Diffstat (limited to 'kernel/byterun')
| -rw-r--r-- | kernel/byterun/coq_instruct.h | 4 | ||||
| -rw-r--r-- | kernel/byterun/int64_emul.h | 2 | ||||
| -rw-r--r-- | kernel/byterun/int64_native.h | 2 | ||||
| -rw-r--r-- | kernel/byterun/libcoqrun.clib | 4 |
4 files changed, 10 insertions, 2 deletions
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 |