Fix an exponential behavior in guard checker for cofixpoints.

I had introduced it by mistake due to my OCaml dyslexia :)
Thanks to Enrico and Arnaud for saving my day!
More optimization in guard checking.

When dynamically computing the recarg tree, we now prune it according to the
inferred tree. Compilation of CompCert is now ok.
One more optimization for guard checking of cofixpoints.

In check_one_cofix, we now avoid calling dest_subterms each time we meet a
constructor by storing both the current tree (needed for the new criterion)
and a precomputed array of trees for subterms.