Do not recompute twice the whnf of terms in conversion.

This performance bug was introduced 9 years ago in a8b0345, where the
responsibility of normalizing the term went from ccnv to eqappr in Reduction.
As a result, all recursive calls to eqappr that were preemptively reducing the
term ended up calling whd_stack twice, once by themselves, and once in the
subsequent call to eqappr.

This caused an important slowdown for conversion-intensive proofs, as the
whd_stack calls CClosure.zip to perfom in-place term sharing, leading to
useless huge re-allocations and repetitive write barriers.

Now that eqappr always head-normalizes the term beforehand, we simply don't
call whd_stack anymore when jumping to eqappr.

0 files changed, 0 insertions, 0 deletions