| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Set up the same test infrastructure as in Boogie. |  wuestholz | 2014-05-29 |
| | | |||
| * | Members included from different files are now internally marked with an ↵ | Rustan Leino | 2014-04-19 |
| | | | | | | | | IncludeToken; the previous scheme of using {:verify false} is no longer used. This makes "include" work with refinement features. Filenames of included files used in error messages are now what the user wrote, rather than absolute paths (which not only don't look so good, but are also problematic in comparing test output on different machines). Added dafny0/Includee.dfy to the test suite as well -- might as well include it, too, to get checked. | ||
| * | Add support for the "include" keyword, which accepts a (possibly relative) path |  Bryan Parno | 2013-12-10 |
| to another Dafny file. That file's functions and methods are included but not checked. This is intended to support incremental verification on a per-file basis. | |||
 |
index : debian-dafny | |
| Debian packaging for Dafny |
| summaryrefslogtreecommitdiff |