]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e6c3035) | patch
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
treecba69b75849269ec7cbf00c83db42f7b91f510batree | snapshot
parente6c30351b99a9732c0aa5df361d1510b998afb76commit | diff
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 diff | blob | history
helm/software/components/disambiguation/disambiguate.ml diff | blob | history
helm/software/components/disambiguation/disambiguate.mli diff | blob | history
helm/software/components/disambiguation/multiPassDisambiguator.ml diff | blob | history
helm/software/components/disambiguation/multiPassDisambiguator.mli diff | blob | history
helm/software/components/ng_disambiguation/nCicDisambiguate.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.