]> 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)
commited936515481f5035fde443f4aee55b86e427cef4
tree1019746e362a1173a48f1b0213cf6b01686847e8
parentd7bcd7edff17b405b07ea17a38101c699e27bf8d
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.
helm/software/components/cic_proof_checking/cicReduction.ml