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