From beb417ffd2ab9acb708c4e54dd28363bcb613853 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 13 Jul 2018 02:09:56 +0200
Subject: Store the {struct} inductive type in native fixpoint AST.

---
 kernel/nativeinstr.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/nativeinstr.mli')

diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli
index eaad8ee0c2..5075bd3d14 100644
--- a/kernel/nativeinstr.mli
+++ b/kernel/nativeinstr.mli
@@ -36,7 +36,7 @@ and lambda =
   | 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 *)
-- 
cgit v1.2.3