]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2d4775a) | 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)
commit6b018dd85365fcb4af1bb538c3198978c01cb24e
tree88f572fbf910222e7e2828801095bab7454b235dtree | snapshot
parent2d4775af99f2a2c4a0e7fc7f5cde32a08af4a592commit | 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.
components/cic_disambiguation/disambiguateChoices.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.