diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-26 13:07:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-26 13:07:34 +0200 |
| commit | 4a82de3b5b9d4a1a0830291b5b9a485bf2a16ded (patch) | |
| tree | 15ff7464cc5a250fbb6ed2a10887d34cfb62a8a4 /kernel/byterun/coq_instruct.h | |
| parent | 95429d01a8f47f5f9d1ecee3b452d920e1e1af22 (diff) | |
| parent | 2290dbb9c95b63e693ced647731623e64297f5c8 (diff) | |
Merge branch 'v8.5' into v8.6
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 885594ac7..d92e85fdf 100644 --- a/kernel/byterun/coq_instruct.h +++ b/kernel/byterun/coq_instruct.h @@ -39,6 +39,7 @@ enum instructions { GETFIELD0, GETFIELD1, GETFIELD, SETFIELD0, SETFIELD1, SETFIELD, PROJ, + ENSURESTACKCAPACITY, CONST0, CONST1, CONST2, CONST3, CONSTINT, PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT, ACCUMULATE, |