diff options
| -rw-r--r-- | kernel/nativeconv.ml | 2 | ||||
| -rw-r--r-- | kernel/nativevalues.ml | 12 | ||||
| -rw-r--r-- | kernel/nativevalues.mli | 2 | ||||
| -rw-r--r-- | pretyping/nativenorm.ml | 2 |
4 files changed, 8 insertions, 10 deletions
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 diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index ae66362ca..95a8fc5a4 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -153,8 +153,7 @@ let accu_nargs (k:accumulator) = let args_of_accu (k:accumulator) = let nargs = accu_nargs k in let f i = (Obj.magic (Obj.field (Obj.magic k) (nargs-i+2)) : t) in - let t = Array.init nargs f in - Array.to_list t + Array.init nargs f let is_accu x = let o = Obj.repr x in @@ -179,11 +178,10 @@ let force_cofix (cofix : t) = let atom = atom_of_accu accu in match atom with | Acofix(typ,norm,pos,f) -> - let f = ref f in - let args = List.rev (args_of_accu accu) in - List.iter (fun x -> f := !f x) args; - let v = !f (Obj.magic ()) in - set_atom_of_accu accu (Acofixe(typ,norm,pos,v)); + let args = args_of_accu accu in + let f = Array.fold_right (fun arg f -> f arg) args f in + let v = f (Obj.magic ()) in + set_atom_of_accu accu (Acofixe(typ,norm,pos,v)); v | Acofixe(_,_,_,v) -> v | _ -> cofix diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 18b877745..17d6978cd 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -84,7 +84,7 @@ val napply : t -> t array -> t val dummy_value : unit -> t val atom_of_accu : accumulator -> atom -val args_of_accu : accumulator -> t list +val args_of_accu : accumulator -> t array val accu_nargs : accumulator -> int val cast_accu : t -> accumulator diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 79e0afa72..18ae22ab6 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -246,7 +246,7 @@ and nf_args env sigma accu t = let c = nf_val env sigma arg dom in (subst1 c codom, c::l) in - let t,l = List.fold_right aux (args_of_accu accu) (t,[]) in + let t,l = Array.fold_right aux (args_of_accu accu) (t,[]) in t, List.rev l and nf_bargs env sigma b t = |