]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9501838) | patch
Fixed bug in notation: when a notation is applied to more arguments than expected...
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 27 Nov 2006 15:01:04 +0000 (15:01 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 27 Nov 2006 15:01:04 +0000 (15:01 +0000)
commitf9ec0bd466364409050ffccc94e9cb863e2ddf28
treebff1fdc9438c108a5d53da3a77a8892472ef596atree | snapshot
parent950183890e7b5ff953b3756b21f655bfe3955f20commit | diff
Fixed bug in notation: when a notation is applied to more arguments than expected this is not necessarily a problem: I just create a new application on the fly.
helm/software/components/cic_disambiguation/disambiguateChoices.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.