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