aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/byterun/coq_instruct.h
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/byterun/coq_instruct.h')
-rw-r--r--kernel/byterun/coq_instruct.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h
index e224a1080..d1136b2dc 100644
--- a/kernel/byterun/coq_instruct.h
+++ b/kernel/byterun/coq_instruct.h
@@ -49,6 +49,7 @@ enum instructions {
HEAD0INT31, TAIL0INT31,
ISCONST, ARECONST,
COMPINT31, DECOMPINT31,
+ ORINT31, ANDINT31, XORINT31,
/* /spiwack */
STOP
};