summaryrefslogtreecommitdiff
path: root/Test/dafny0/Compilation.dfy.expect
Commit message (Collapse)AuthorAge
* Fixed compilation of equality between reference typesGravatar leino2015-11-11
|
* Implemented resolution, verification, and (poorly performing) compilation of ↵Gravatar leino2015-10-05
| | | | | | | existential if guards. Fixed bugs in ghost checks involving comprehensions and attributes. Added SubstituteBoundedPool method.
* Allow underscores in numeric literals (and in field/destructor names that ↵Gravatar leino2014-10-23
| | | | | | are written as numeric strings). The underscores have no semantic meaning, but can help a human parse the numbers.
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29