]> matita.cs.unibo.it Git - helm.git/commitdiff
The aliases and multi_aliases in the lexicon status are now
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 3 Dec 2008 22:53:01 +0000 (22:53 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 3 Dec 2008 22:53:01 +0000 (22:53 +0000)
LexiconAst.alias_spec (they used to be DisambiguateTypes.codomain_item).
Benefit: it is now possible to use the very same set of aliases both for the
new and old terms. Moreover, this commits simplifies quite a bit of code.

Known bugs: when clicking the "OK" button in the error message disambiguation
window, an assertion is often raised. When the assertion is not raised, the
set of aliases that are printed are not syntactically/semantically correct.


No differences found