Merge branch 'v8.5' into trunk

1 files changed, 3 insertions, 0 deletions

diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index d9998c89e8..745ef311b0 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 ? *)