aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/nativecode.ml')
-rw-r--r--kernel/nativecode.ml2
1 files changed, 1 insertions, 1 deletions
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
..