summaryrefslogtreecommitdiff
path: root/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect
Commit message (Collapse)AuthorAge
* Implement {:nowarn}, clarify some messages, and add a few testsGravatar Clément Pit--Claudel2015-08-28
|
* s/loops with/may loop with/Gravatar Clément Pit--Claudel2015-08-23
|
* Make `old` a special case for trigger generation.Gravatar Clément Pit--Claudel2015-08-21
Old is particular, because in old(g(f(x))), the triggers are old(g(x)) and old(f(x)). This has a number of implications; see the new tests files for more information.