]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5e4deb6) | patch
Missing optimization implemented: before starting to analyze the disambiguation
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 18 Oct 2006 17:39:48 +0000 (17:39 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 18 Oct 2006 17:39:48 +0000 (17:39 +0000)
commit7a974bd5775acf432e4074f32a99cc08d42b667f
tree086e360f8d99b4126856d01e3a4141a9c14b541btree | snapshot
parent5e4deb64b7cae2df0a51425e3768ca316c297953commit | diff
Missing optimization implemented: before starting to analyze the disambiguation
domain we try first without interpreting any symbol. This way we can avoid
lot of refinements when the information in the uninterpreted term already
tells us that every instance will not be well typed.
components/cic_disambiguation/disambiguate.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.