Imported Upstream version 8.9.0upstream/8.9.0upstream

1 files changed, 3 insertions, 3 deletions

diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli
index c319be32..2d8e2ba2 100644
--- a/kernel/nativeinstr.mli
+++ b/kernel/nativeinstr.mli
@@ -25,18 +25,18 @@ and lambda =
   | Lrel          of Name.t * int 
   | Lvar          of Id.t
   | Lmeta         of metavariable * lambda (* type *)
-  | Levar         of Evar.t * lambda (* type *) * lambda array (* arguments *)
+  | Levar         of Evar.t * lambda array (* arguments *)
   | Lprod         of lambda * lambda 
   | Llam          of Name.t array * lambda  
   | Llet          of Name.t * lambda * lambda
   | Lapp          of lambda * lambda array
   | Lconst        of prefix * pconstant
-  | Lproj         of prefix * Constant.t (* prefix, projection name *)
+  | Lproj         of prefix * inductive * int (* prefix, inductive, index starting from 0 *)
   | Lprim         of prefix * Constant.t * CPrimitives.t * lambda array
   | Lcase         of annot_sw * lambda * lambda * lam_branches 
                   (* annotations, term being matched, accu, branches *)
   | Lif           of lambda * lambda * lambda
-  | Lfix          of (int array * int) * fix_decl 
+  | Lfix          of (int array * (string * inductive) array * int) * fix_decl
   | Lcofix        of int * fix_decl (* must be in eta-expanded form *)
   | Lmakeblock    of prefix * pconstructor * int * lambda array
                   (* prefix, constructor name, constructor tag, arguments *)