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

---
 kernel/nativecode.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/nativecode.ml')

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 8d69eacbc..b09cd3f79 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1142,7 +1142,7 @@ let ml_of_instance instance u =
       mkMLapp (MLapp (MLglobal cn, fv_args env fvn fvr)) [|force|]
   | Lif(t,bt,bf) -> 
       MLif(ml_of_lam env l t, ml_of_lam env l bt, ml_of_lam env l bf)
-  | Lfix ((rec_pos,start), (ids, tt, tb)) ->
+  | Lfix ((rec_pos, inds, start), (ids, tt, tb)) ->
       (* let type_f fvt = [| type fix |] 
          let norm_f1 fv f1 .. fn params1 = body1
 	 ..
-- 
cgit v1.2.3