| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Hover text includes #[_k-1] suffix for terms rewritten in prefix ↵ |  Rustan Leino | 2015-10-02 |
| | | | | | | | | predicates/lemmas (this fixes an item from the wishlist). Include in hover text the extreme predicates for which an extreme lemmas has been rewritten (but don't include ==# in this list--or should it perhaps be included?). Under a (temporary) switch /rewriteFocalPredicates, each use of a focal predicate P in a prefix lemma is rewritten into P#[_k-1]. | ||
| * | Fix: Unify column numbers in Dafny's errors |  Clément Pit--Claudel | 2015-07-23 |
| | | | | | | | | | | Dafny counts from 0, but Boogie counts from 1. Tokens are 1-based. Thus when we print tokens, we need to decrement the column number. This was done for resolver errors, but not for verification or parsing errors. In addition, parsing errors were inconsistent with resolution errors case-wise. Unfortunately, the fix affects the output of many tests. | ||
| * | Set up the same test infrastructure as in Boogie. | wuestholz | 2014-05-29 |
 |
index : debian-dafny | |
| Debian packaging for Dafny |
| summaryrefslogtreecommitdiff |