]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 36c07ee) | patch
In guarded by destructors, avoid computing the (whd ~delta:true) unless the
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 28 Apr 2008 17:43:33 +0000 (17:43 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 28 Apr 2008 17:43:33 +0000 (17:43 +0000)
commitebb2f4bda5f7c5c7fc26d3aa1e17312f8900da4a
tree1296a63081e1c3521eca7ae99b9f907a82662419tree | snapshot
parent36c07ee08f1d0e63719f69f41ee6537f47f2c265commit | diff
In guarded by destructors, avoid computing the (whd ~delta:true) unless the
check fails. This is a major speed up, for instance for
cic:/Coq/ZArith/Zsqrt/sqrtrempos.con
helm/software/components/cic_proof_checking/cicTypeChecker.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.