]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c394cbf) | patch
"Performance bug" fixed: I removed a whd in the does_not_occur function.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 27 Mar 2006 14:01:26 +0000 (14:01 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 27 Mar 2006 14:01:26 +0000 (14:01 +0000)
commit9af2c02b054a92804da88cb06d6699ce21b943c0
tree99b7755a4abf22ca75c0c793be543f7d33715da6tree | snapshot
parentc394cbfac807c8448910935f4fde5e700c76f531commit | diff
"Performance bug" fixed: I removed a whd in the does_not_occur function.
Consequences:
  1. incredible speed-up in the type-checking of certain inductive types
  2. "dummy" occurrences (i.e. occurrences that are doomed to disappear because
     of reduction) are now rejected (they used to be accepted). Coq has the
     same behaviour.
components/cic_proof_checking/cicTypeChecker.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.