]> matita.cs.unibo.it Git - helm.git/commit
Brand new implementation based on functors taking a strategy in input.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 2 Dec 2002 14:35:13 +0000 (14:35 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 2 Dec 2002 14:35:13 +0000 (14:35 +0000)
commitdb593c40165a5ac71b6aa87e43e90b8b45e8ed59
tree6463921be48c38de129e44c547af5d21d0d714dc
parent2d2f5481683a16008aa7fbddbe0c21ad854b8fe0
Brand new implementation based on functors taking a strategy in input.
Several different strategies have been implemented. Unfortunately many
of them are incomparable and there are critical examples where only some
of them terminate in reasonable time.

Removing the functor/module stuff does not bring any sensible performance
improvement even for simple strategies (where most of the functions are
just identity fuctions that can be inlined when not crossing functor
boundaries).
helm/ocaml/cic_proof_checking/cicReductionMachine.ml