diff options
Diffstat (limited to 'kernel/cbytecodes.mli')
| -rw-r--r-- | kernel/cbytecodes.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index d9998c89e..745ef311b 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -25,6 +25,7 @@ val last_variant_tag : tag type structured_constant = | Const_sorts of sorts | Const_ind of pinductive + | Const_proj of Constant.t | Const_b0 of tag | Const_bn of tag * structured_constant array @@ -72,6 +73,8 @@ type instruction = | Ksetfield of int | Kstop | Ksequence of bytecodes * bytecodes + | Kproj of int * Constant.t (** index of the projected argument, + name of projection *) (** spiwack: instructions concerning integers *) | Kbranch of Label.t (** jump to label, is it needed ? *) |