aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cClosure.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-01-30 14:20:48 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-02-02 14:01:33 +0100
commitc7026ec14f94875fc4b58951fa8bec628fcfac42 (patch)
treed85ea0027dafba9301220d75ed8ed84e64d73c90 /kernel/cClosure.mli
parent76aff3cbe39da657abb1f559b8ba411a49aab317 (diff)
Use whd-all on rigid-flex conversion.
This heuristic is justified by the fact that during a conversion check between a flexible and a rigid term, the flexible one is eventually going to be fully weak-head normalized. So in this case instead of performing many small reduction steps on the flexible term, we perform full weak-head reduction, including delta. It is slightly more efficient in actual developments, and it fixes a corner case encountered by Jason Gross. Fixes #6667: Kernel conversion is much, much slower than `Eval lazy`.
Diffstat (limited to 'kernel/cClosure.mli')
0 files changed, 0 insertions, 0 deletions