Allocation-friendly detyping of term arrays.

This is important for externalization big terms. We were indeed allocating
twice as much as needed lists for the application node case, as the
Array.map_to_list function is exactly List.map o Array.to_list.

We could probably tweak this function instead, at the expense that order of
evaluation is not guaranteed. I'm not willing to do that though.

0 files changed, 0 insertions, 0 deletions