]> matita.cs.unibo.it Git - helm.git/commit
disambiguation takes ~mk_localization_tbl and not ~localization_tbl, thus can
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 5 Dec 2008 11:26:55 +0000 (11:26 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 5 Dec 2008 11:26:55 +0000 (11:26 +0000)
commit93ce01455cfeba6b29e3c8a57e28f56559fb891d
treecba69b75849269ec7cbf00c83db42f7b91f510ba
parente6c30351b99a9732c0aa5df361d1510b998afb76
disambiguation takes ~mk_localization_tbl and not ~localization_tbl, thus can
create the hashtable when needed (after every interpretation)
helm/software/components/cic_disambiguation/cicDisambiguate.ml
helm/software/components/disambiguation/disambiguate.ml
helm/software/components/disambiguation/disambiguate.mli
helm/software/components/disambiguation/multiPassDisambiguator.ml
helm/software/components/disambiguation/multiPassDisambiguator.mli
helm/software/components/ng_disambiguation/nCicDisambiguate.ml