]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 730824d) | patch
Huge speed-up in conversion: the old conversion strategy is set back.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 29 Mar 2006 16:26:32 +0000 (16:26 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 29 Mar 2006 16:26:32 +0000 (16:26 +0000)
commita484672e530900bb3b3aa02f9fff5fedd9fb06a4
tree7b85fdf843241293967b9b81c0c247a8547a4232tree | snapshot
parent730824d3dc60ff3d6d7cff3f5d11c3621eb0f552commit | diff
Huge speed-up in conversion: the old conversion strategy is set back.
 1. try to "convert" the two terms recursively without performing reduction
 2. if it fails, do a whd and try again
The overall result on the library of Coq is really remarkable.
components/cic_proof_checking/cicReduction.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.