]> matita.cs.unibo.it Git - helm.git/commit
New reduction strategy: the new reduction strategy behaves as the previous
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 10 Jul 2007 18:48:14 +0000 (18:48 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 10 Jul 2007 18:48:14 +0000 (18:48 +0000)
commit122d4b9f48a45a56e87818e44dee5e23e753524a
tree13ada1d056276078a293681329a41a2bc6ef3391
parent2ab051e4693e68f96481eac5b14872f573ad4b7f
New reduction strategy: the new reduction strategy behaves as the previous
one (performing both CVN and CBV in parallel), but it is much more lazy.
In particular, unwinding is never performed twice on the same term.
On assembly/assembly.ma this seems to solve every performance problem.
Let's see what happens this night with the benchmarks.
components/cic_proof_checking/cicReduction.ml