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 8c5ab0ecb..dc3a88818 100644
--- a/kernel/byterun/coq_instruct.h
+++ b/kernel/byterun/coq_instruct.h
@@ -37,6 +37,7 @@ enum instructions {
GETFIELD0, GETFIELD1, GETFIELD,
SETFIELD0, SETFIELD1, SETFIELD,
PROJ,
+ ENSURESTACKCAPACITY,
CONST0, CONST1, CONST2, CONST3, CONSTINT,
PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT,
ACCUMULATE,