aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/byterun/coq_fix_code.h
diff options
context:
space:
mode:
authorGravatar gregoire <gregoire@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-11-22 09:10:51 +0000
committerGravatar gregoire <gregoire@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-11-22 09:10:51 +0000
commita215993ad9e073fc09825742494ec06a9f8d6c84 (patch)
treea104125a1b9029473a05a36e70cfe9ce9e9c5212 /kernel/byterun/coq_fix_code.h
parent7371c43d5b065e83bbaaba584dc163cac2005802 (diff)
compatibility with POWERPC
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6338 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/byterun/coq_fix_code.h')
-rw-r--r--kernel/byterun/coq_fix_code.h12
1 files changed, 7 insertions, 5 deletions
diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h
index e3296c0da..035d5b9b1 100644
--- a/kernel/byterun/coq_fix_code.h
+++ b/kernel/byterun/coq_fix_code.h
@@ -18,11 +18,13 @@ void * coq_stat_alloc (asize_t sz);
#ifdef THREADED_CODE
extern char ** coq_instr_table;
extern char * coq_instr_base;
-#define Is_instruction(i1,i2) \
- (*i1 == (opcode_t)(coq_instr_table[i2] - coq_instr_base))
-#else
-#define Is_instruction(i1,i2) (*i1 == i2)
-#endif
+void init_arity();
+#define VALINSTR(instr) ((opcode_t)(coq_instr_table[instr] - coq_instr_base))
+#else
+#define VALINSTR(instr) instr
+#endif /* THREADED_CODE */
+
+#define Is_instruction(pc,instr) (*pc == VALINSTR(instr))
value coq_tcode_of_code(value code, value len);
value coq_makeaccu (value i);