diff options
Diffstat (limited to 'kernel/byterun/coq_instruct.h')
-rw-r--r-- | kernel/byterun/coq_instruct.h | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h index d3b07526..89616c5f 100644 --- a/kernel/byterun/coq_instruct.h +++ b/kernel/byterun/coq_instruct.h @@ -22,18 +22,20 @@ enum instructions { PUSH_RETADDR, APPLY, APPLY1, APPLY2, APPLY3, APPTERM, APPTERM1, APPTERM2, APPTERM3, - RETURN, RESTART, GRAB, GRABREC, COGRAB, - CLOSURE, CLOSUREREC, + RETURN, RESTART, GRAB, GRABREC, + CLOSURE, CLOSUREREC, CLOSURECOFIX, OFFSETCLOSUREM2, OFFSETCLOSURE0, OFFSETCLOSURE2, OFFSETCLOSURE, PUSHOFFSETCLOSUREM2, PUSHOFFSETCLOSURE0, PUSHOFFSETCLOSURE2, PUSHOFFSETCLOSURE, GETGLOBAL, PUSHGETGLOBAL, - MAKEBLOCK, MAKEBLOCK1, MAKEBLOCK2, MAKEBLOCK3, - MAKESWITCHBLOCK, MAKEACCU, MAKEPROD, - FORCE, SWITCH, PUSHFIELD, + MAKEBLOCK, MAKEBLOCK1, MAKEBLOCK2, MAKEBLOCK3, MAKEBLOCK4, + SWITCH, PUSHFIELDS, + GETFIELD0, GETFIELD1, GETFIELD, + SETFIELD0, SETFIELD1, SETFIELD, CONST0, CONST1, CONST2, CONST3, CONSTINT, PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT, - ACCUMULATE, ACCUMULATECOND, STOP + ACCUMULATE, ACCUMULATECOND, + MAKESWITCHBLOCK, MAKEACCU, MAKEPROD, STOP }; #endif /* _COQ_INSTRUCT_ */ |