diff options
author | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
tree | 591e9e512063e34099782e2518573f15ffeac003 /kernel/byterun/coq_instruct.h | |
parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
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_ */ |