]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (from: 9af2c02)
"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)
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.


No differences found
Unnamed repository; edit this file 'description' to name the repository.