]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a3ca416) | patch
Lookup_in_library implemented for new objects. Basically, this stupid (??),
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 25 Apr 2009 22:30:39 +0000 (22:30 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 25 Apr 2009 22:30:39 +0000 (22:30 +0000)
commite02c6eaf8d50025c3be8bbf6988ab8b2a37b40da
tree30e396f265ad8b2f984954391e9f33536a5f9da7tree | snapshot
parenta3ca416fdbe04b22a921dfd18b55e67564b045cccommit | diff
Lookup_in_library implemented for new objects. Basically, this stupid (??),
inefficient (??) implementation just keeps an associative list that maps names
to URIs and is used to resolve names in the library. This functionality is
provided by ng_kernel/nCicLibrary.

Note: automatic addition of preferences is not there yet.
Thus you need to activate lookup in library to see it working.
helm/software/components/grafite_parser/grafiteDisambiguate.ml diff | blob | history
helm/software/components/ng_kernel/nCicLibrary.ml diff | blob | history
helm/software/components/ng_kernel/nCicLibrary.mli diff | blob | history
helm/software/matita/tests/ng_commands.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.