]> 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:21:07 +0000 (17:21 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 15 Sep 2005 17:21:07 +0000 (17:21 +0000)
commit8539d00ff2ed0ffd9b7a08ac8e62376e88987960
tree5c2347527e252b93fc8688456d7d4f4130ee3e28
parentc6a7eec919569a87c3335b83b5d531901877fd9e
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/ocaml/cic_disambiguation/disambiguate.ml
helm/ocaml/cic_disambiguation/disambiguate.mli
helm/ocaml/cic_disambiguation/disambiguatePp.ml
helm/ocaml/cic_disambiguation/disambiguatePp.mli
helm/ocaml/cic_disambiguation/disambiguateTypes.ml
helm/ocaml/cic_disambiguation/disambiguateTypes.mli