]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a1b87ca) | patch
#### EXPERIMENTAL COMMIT ####
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 29 Mar 2006 14:44:00 +0000 (14:44 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 29 Mar 2006 14:44:00 +0000 (14:44 +0000)
commit730824d3dc60ff3d6d7cff3f5d11c3621eb0f552
tree78f78d71d43d38163b31475008d98754b73b3137tree | snapshot
parenta1b87ca1225a74b0d7b913e38c8ff6004737448bcommit | diff
#### EXPERIMENTAL COMMIT ####
Added a potentially dangerous ~expand_beta_redexes flag to
CicSubstitution.subst. If used carefully, it enormously speeds up
the type-checking of many theorems (since a very frequent conversion test
happens between a beta-redex and its contractum).
components/cic_proof_checking/cicReduction.ml diff | blob | history
components/cic_proof_checking/cicSubstitution.ml diff | blob | history
components/cic_proof_checking/cicSubstitution.mli diff | blob | history
components/cic_proof_checking/cicTypeChecker.ml diff | blob | history
components/cic_proof_checking/freshNamesGenerator.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.