aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--kernel/nativelambda.ml5
1 files changed, 1 insertions, 4 deletions
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index f3b483467d..aa30a01134 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -381,10 +381,7 @@ let makeblock env ind tag nparams arity args =
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)
+ Lparray (args, def)
(* Translation of constants *)