]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 61acdea) | patch
Bug fixed: aliases for numbers were no longer handled correctly (since 0 was
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 22 Sep 2006 16:28:39 +0000 (16:28 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 22 Sep 2006 16:28:39 +0000 (16:28 +0000)
commit59c85666e58d43d1dce56a2456db5f1ec223c1c3
tree49435469db07d366b7100bcde8ca244a90471863tree | snapshot
parent61acdea2419b3889096fd1e41275062b78253af0commit | diff
Bug fixed: aliases for numbers were no longer handled correctly (since 0 was
a wildcard only for symbols).
components/cic_disambiguation/disambiguate.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.