]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ebb2f4b) | patch
Avoid (whd ~delta:true) during guarded_by_destructors as much as possible.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 28 Apr 2008 17:52:04 +0000 (17:52 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 28 Apr 2008 17:52:04 +0000 (17:52 +0000)
commitfbadb3454a52d879edc58a4a09ca46c1e77dce2f
tree746e358022bcdeef11db93e8e297d62225393c77tree | snapshot
parentebb2f4bda5f7c5c7fc26d3aa1e17312f8900da4acommit | diff
Avoid (whd ~delta:true) during guarded_by_destructors as much as possible.
Note: it is better to check again if this commit is fully correct (i.e.
w.r.t. the catch-all case in the main "match ... with" of the aux function).
helm/software/components/ng_kernel/nCicTypeChecker.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.