]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 238b544) | patch
It is now possible to declare new aliases using the old syntax
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 25 Apr 2009 21:24:50 +0000 (21:24 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 25 Apr 2009 21:24:50 +0000 (21:24 +0000)
commita3ca416fdbe04b22a921dfd18b55e67564b045cc
tree82fc2fb5e15c5c78facbc73c38ea37faa58f84b3tree | snapshot
parent238b544db1786fbc68354fd62aa6b05983906997commit | diff
It is now possible to declare new aliases using the old syntax
(maybe confusing, but a string is a string). Thus much code becomes
useless in GrafiteDisambiguate. But it will be moved in the next commit
to nCicLibrary to implement the nlookup_in_library function.
helm/software/components/grafite_parser/grafiteDisambiguate.ml diff | blob | history
helm/software/components/grafite_parser/grafiteParser.ml diff | blob | history
helm/software/matita/tests/ng_commands.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.