summaryrefslogtreecommitdiff
path: root/Binaries/DafnyPrelude.bpl
diff options
context:
space:
mode:
authorGravatar MichalMoskal <unknown>2009-12-17 01:17:59 +0000
committerGravatar MichalMoskal <unknown>2009-12-17 01:17:59 +0000
commit9447617aefbe9706b0d74a827181976e4b9e9d26 (patch)
tree471ea6938e90be46af5e6ce8e7ca88de1081c977 /Binaries/DafnyPrelude.bpl
parentfa8cb4c335668f180fa2c181ca6bb1ad87b54c4a (diff)
Allow ":" in addition to "returns" in function definitions. Make the pretty-printer use ":" not "returns".
Allow foo(x,y,z:int,p,q:ptr) kind of syntax in function definitions. Consequently foo(int,y:bool) is no longer allowed. Update the testsuite to match that.
Diffstat (limited to 'Binaries/DafnyPrelude.bpl')
0 files changed, 0 insertions, 0 deletions