]> matita.cs.unibo.it Git - helm.git/commit
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
treebff1fdc9438c108a5d53da3a77a8892472ef596a
parent950183890e7b5ff953b3756b21f655bfe3955f20
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