1 files changed, 22 insertions, 2 deletions
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 3819cfd8ee..b00b96018f 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -40,6 +40,7 @@ type lambda =
   | Lfix          of (int array * (string * inductive) array * int) * fix_decl
   | Lcofix        of int * fix_decl
   | Lint          of int (* a constant constructor *)
+  | Lparray       of lambda array * lambda
   | Lmakeblock    of prefix * inductive * int * lambda array
                   (* prefix, inductive name, constructor tag, arguments *)
         (* A fully applied non-constant constructor *)
@@ -187,6 +188,10 @@ let map_lam_with_binders g f n lam =
   | Levar (evk, args) ->
     let args' = Array.Smart.map (f n) args in
     if args == args' then lam else Levar (evk, args')
+  | Lparray (p,def) ->
+      let p' = Array.Smart.map (f n) p in
+      let def' = f n def in
+      if def' == def && p == p' then lam else Lparray (p', def')
 
 (*s Lift and substitution *)
 
@@ -377,6 +382,12 @@ let makeblock env ind tag nparams arity args =
     let prefix = get_mind_prefix env (fst ind) in
     Lmakeblock(prefix, ind, tag, args)
 
+let makearray args def =
+  try
+    let p = Array.map get_value args in
+    Lval (Nativevalues.parray_of_array p (get_value def))
+  with Not_found -> Lparray (args, def)
+
 (* Translation of constants *)
 
 let rec get_alias env (kn, u as p) =
@@ -400,8 +411,13 @@ let expand_prim env kn op arity =
 
 let lambda_of_prim env kn op args =
   let arity = CPrimitives.arity op in
-  if Array.length args >= arity then prim env kn op args
-  else mkLapp (expand_prim env kn op arity) args
+  match Int.compare (Array.length args) arity with
+  | 0 -> prim env kn op args
+  | x when x > 0 ->
+    let prim_args = Array.sub args 0 arity in
+    let extra_args = Array.sub args arity (Array.length args - arity) in
+    mkLapp(prim env kn op prim_args) extra_args
+  | _ -> mkLapp (expand_prim env kn op arity) args
 
 (*i Global environment *)
 
@@ -589,6 +605,10 @@ let rec lambda_of_constr cache env sigma c =
 
   | Float f -> Lfloat f
 
+  | Array (_u, t, def, _ty) ->
+    let def = lambda_of_constr cache env sigma def in
+    makearray (lambda_of_args cache env sigma 0 t) def
+
 and lambda_of_app cache env sigma f args =
   match kind f with
   | Const (_kn,_u as c) ->