]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: beb4e1e) | 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)
commit9b453fb080b106df17ac71f7afffe50bbf631e1d
treed39e699c8b8cc353eb68436a98b2de12ff99b425tree | snapshot
parentbeb4e1e9549d5b43e24907dc86c7ef899e487a3ccommit | diff
Bug fixed: aliases for numbers were no longer handled correctly (since 0 was
a wildcard only for symbols).
helm/software/components/cic_disambiguation/disambiguate.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.