]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4e3d7b4) | 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)
commitbbdb53860d667dfba1aab3a6f195d0fcd4a9e818
treec6ae26f73a5376412ed0daff51b3bb8d34dc83d9tree | snapshot
parent4e3d7b4b47f66f0745333bfd4efcb27b4528f4c3commit | 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.
helm/software/components/cic_proof_checking/cicReduction.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.