diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /kernel/byterun/coq_instruct.h | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'kernel/byterun/coq_instruct.h')
-rw-r--r-- | kernel/byterun/coq_instruct.h | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h index e224a108..9cbf4077 100644 --- a/kernel/byterun/coq_instruct.h +++ b/kernel/byterun/coq_instruct.h @@ -38,7 +38,7 @@ enum instructions { SETFIELD0, SETFIELD1, SETFIELD, CONST0, CONST1, CONST2, CONST3, CONSTINT, PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT, - ACCUMULATE, ACCUMULATECOND, + ACCUMULATE, MAKESWITCHBLOCK, MAKEACCU, MAKEPROD, /* spiwack: */ BRANCH, @@ -49,6 +49,7 @@ enum instructions { HEAD0INT31, TAIL0INT31, ISCONST, ARECONST, COMPINT31, DECOMPINT31, + ORINT31, ANDINT31, XORINT31, /* /spiwack */ STOP }; |