summaryrefslogtreecommitdiff
path: root/Test/dafny0/TriggerInPredicate.dfy.expect
Commit message (Collapse)AuthorAge
* In method and iterator specifications, inline top-level predicates (exceptGravatar leino2015-10-24
| | | | protected predicated in cross-module calls) like in other places.
* Suppress many warnings in the test suite.Gravatar Clément Pit--Claudel2015-08-28
| | | | | We already have separate tests for those, and we want the output to be the same with and without /autoTriggers.
* Cleanup indentation of trigger warningsGravatar Clément Pit--Claudel2015-08-19
|
* Clarify the inlining warning.Gravatar Clément Pit--Claudel2015-07-27
|
* Add /autoTriggers to TriggerInPredicate's RUN specificationGravatar Clément Pit--Claudel2015-07-17