summaryrefslogtreecommitdiff
path: root/Source/Dafny/Triggers/TriggerExtensions.cs
Commit message (Expand)AuthorAge
* Further relax the loop detection conditionsGravatar Clément Pit--Claudel2015-08-27
* Small fix: there is no loop in (forall x :: Q(x) && Q(0))Gravatar Clément Pit--Claudel2015-08-27
* Look at the full quantifier to find loops, not just the term.Gravatar Clément Pit--Claudel2015-08-22
* Make `old` a special case for trigger generation.Gravatar Clément Pit--Claudel2015-08-21
* Print matches for triggers as they appear in the bufferGravatar Clément Pit--Claudel2015-08-19
* Fix the equality test for literal expressionsGravatar Clément Pit--Claudel2015-08-19
* Small cleanups, fixes, and refactoringsGravatar Clément Pit--Claudel2015-08-18
* Start committing split quantifiersGravatar Clément Pit--Claudel2015-08-14
* Implement self-loop detectionGravatar Clément Pit--Claudel2015-08-14
* Draft out a more advanced version of trigger generationGravatar Clément Pit--Claudel2015-08-19