]> matita.cs.unibo.it Git - helm.git/commit
Yet another implementation of the single aliases / multi aliases idea.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 15 Sep 2005 17:40:32 +0000 (17:40 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 15 Sep 2005 17:40:32 +0000 (17:40 +0000)
commit8ecc9fb74f80c2f5b3e3c70f0a625e63a48292fb
tree31d387b19ea518522dfe719abcbeb0ae5b369642
parent39eee3ee34bd22321d7b80c2685395345a0957e0
Yet another implementation of the single aliases / multi aliases idea.
The new implementation is much simpler: single aliases are used everywhere
in the disambiguation phase; however, when a term needs to be looked for in
the library, it can be looked in a user-provided multi aliases environment instead.

NOTE: the new implementation fixes a bug of the previous implementation: the
most recent alias in the multi-alias set was printed last in the .moo files,
changing the performances of the system.
helm/matita/matitaDisambiguator.ml
helm/matita/matitaDisambiguator.mli
helm/matita/matitaEngine.ml
helm/matita/matitaMisc.ml
helm/matita/matitaMisc.mli
helm/matita/matitaScript.ml
helm/matita/matitaSync.ml
helm/matita/matitaTypes.ml
helm/matita/matitaTypes.mli