]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8dfe64d) | patch
Revert of the previous situation: when an identifier has no universe all the
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 20 Jul 2006 15:17:46 +0000 (15:17 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 20 Jul 2006 15:17:46 +0000 (15:17 +0000)
commit1efb99c438c14bbda44f7b8dfe169968a18215a5
tree698cd8a1050e0693620684493bf97385b1d96ba5tree | snapshot
parent8dfe64de7854c787c1f226a11e7ed540b0e67d9fcommit | diff
Revert of the previous situation: when an identifier has no universe all the
passes that does not use the library are doomed to fail and the user will
be asked how to instantiate everyn identifier (not withstanding performances).
Now if an identifier has no universe we look for its interpretations in the
library.
components/cic_disambiguation/disambiguate.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.