]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e368ff6) | patch
Big bug fixed: grafiteDisambiguate.add_aliases_for_objects used to add
authorAndrea Asperti <andrea.asperti@unibo.it>
Mon, 8 Nov 2010 12:41:33 +0000 (12:41 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Mon, 8 Nov 2010 12:41:33 +0000 (12:41 +0000)
commit2ab652e8e37ad8459510eeff3741b0b16e00d8fb
tree42cb5f9f873f9e00ba02903d833dddc5e57ff85btree | snapshot
parente368ff6b06dd1ae1ea337d66fa180e5393d5acb0commit | diff
Big bug fixed: grafiteDisambiguate.add_aliases_for_objects used to add
aliases to the status, but not to the .ng.

Fixed, but we probably need a better approach where the addition to the
.ng is performed by the single modules, and not in grafiteEngine as it
is now.
matita/components/grafite_engine/grafiteEngine.ml diff | blob | history
matita/components/ng_disambiguation/grafiteDisambiguate.ml diff | blob | history
matita/components/ng_disambiguation/grafiteDisambiguate.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.