Allocation-friendly detyping of term arrays.
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.

gares/coq,ejgallego/coq,letouzey/coq-wip,JasonGross/coq,SkySkimmer/coq,JasonGross/coq,gares/coq,silene/coq,letouzey/coq-wip,letouzey/coq-wip,JasonGross/coq,JasonGross/coq,Zimmi48/coq,ejgallego/coq,ppedrot/coq,maximedenes/coq,silene/coq,SkySkimmer/coq,gares/coq,gares/coq,Matafou/coq,letouzey/coq-wip,maximedenes/coq,maximedenes/coq,SkySkimmer/coq,silene/coq,ppedrot/coq,ejgallego/coq,coq/coq,letouzey/coq-wip,gares/coq,coq/coq,maximedenes/coq,coq/coq,ppedrot/coq,Zimmi48/coq,ppedrot/coq,maximedenes/coq,Zimmi48/coq,coq/coq,Matafou/coq,SkySkimmer/coq,ejgallego/coq,ppedrot/coq,Matafou/coq,Zimmi48/coq