]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 35c68ef) | patch
Added support for multiple disambiguation passes.
authorStefano Zacchiroli <zack@upsilon.cc>
Mon, 12 Sep 2005 16:06:33 +0000 (16:06 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Mon, 12 Sep 2005 16:06:33 +0000 (16:06 +0000)
commitaa6153d8e480abfe52b00e1bc6bd48ef84c48988
tree2402a4f321fdd19d7497d88593cf92a1328d4dcftree | snapshot
parent35c68efd0a44da26d4aa6ae760ee03712b33dfedcommit | diff
Added support for multiple disambiguation passes.
Actually, passes can differ in:
- whether they use library as fallback for unbound domain items or not
- whether they use multi-aliases or not
- whether they use coercions or not.
The current policy is to postpone the use of coercions as much as possible and to fallback to library only as a last resort.
Passes can be configured from matitaDisambiguator.ml.
helm/matita/matita.txt diff | blob | history
helm/matita/matitaDisambiguator.ml diff | blob | history
helm/matita/matitaDisambiguator.mli diff | blob | history
helm/matita/matitaEngine.ml diff | blob | history
helm/matita/matitaScript.ml diff | blob | history
helm/matita/matitaSync.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.