]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fecaa41) | 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)
commit3add6ac24088e2a1d91a41123f433e2c2b0b796a
tree01fd4ffab35f9bb3a648f08e9f91e1f179bfc092tree | snapshot
parentfecaa410b6226e8614cfef78d0f952e3c676c06ecommit | 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.
helm/software/components/cic_proof_checking/cicTypeChecker.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.