diff options
Diffstat (limited to 'kernel/byterun/coq_instruct.h')
| -rw-r--r-- | kernel/byterun/coq_instruct.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h index 00156ebe8..8a45e9739 100644 --- a/kernel/byterun/coq_instruct.h +++ b/kernel/byterun/coq_instruct.h @@ -42,6 +42,7 @@ enum instructions { SUBINT31, SUBCINT31, SUBCARRYCINT31, MULCINT31, MULINT31, DIV21INT31, DIVINT31, ADDMULDIVINT31, COMPAREINT31, + HEAD0INT31, TAIL0INT31, ISCONST, ARECONST, COMPINT31, DECOMPINT31, /* /spiwack */ |