From 76579aff8f8534cbc990b5ea2652b33655512213 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 30 Jan 2018 10:05:14 +0100 Subject: [native_compute] Remove useless conversion to list in reification. --- kernel/nativeconv.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/nativeconv.ml') diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 9f9102f7d..6c755290d 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -54,7 +54,7 @@ and conv_accu env pb lvl k1 k2 cu = conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu else let cu = conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu in - List.fold_right2 (conv_val env CONV lvl) (args_of_accu k1) (args_of_accu k2) cu + Array.fold_right2 (conv_val env CONV lvl) (args_of_accu k1) (args_of_accu k2) cu and conv_atom env pb lvl a1 a2 cu = if a1 == a2 then cu -- cgit v1.2.3