summaryrefslogtreecommitdiff
path: root/Source/Dafny/Triggers
Commit message (Expand)AuthorAge
* Implement {:nowarn}, clarify some messages, and add a few testsGravatar Clément Pit--Claudel2015-08-28
* Tiny cleanup in TriggersCollectorGravatar Clément Pit--Claudel2015-08-27
* 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
* Improve the redundancy detection algorithm used while constructing sets of termsGravatar Clément Pit--Claudel2015-08-26
* s/loops with/may loop with/Gravatar Clément Pit--Claudel2015-08-23
* Make quantifier splitting a two step processGravatar Clément Pit--Claudel2015-08-23
* Shallow-copy quantifier attributes when splittingGravatar Clément Pit--Claudel2015-08-23
* Add a sanity check in QuantifiersCollectionGravatar Clément Pit--Claudel2015-08-23
* Improve error reporting for split quantifiersGravatar Clément Pit--Claudel2015-08-23
* Allow MultiSelectExpr as quantifier headsGravatar Clément Pit--Claudel2015-08-23
* Trivial code cleanupGravatar Clément Pit--Claudel2015-08-23
* 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
* Rephrase the message about triggers being rejected because they are too strongGravatar Clément Pit--Claudel2015-08-21
* Allow display expressions as trigger termsGravatar Clément Pit--Claudel2015-08-21
* Cleanup a number of FIXMEs that I had left in the codeGravatar Clément Pit--Claudel2015-08-20
* Implement the SelectTrigger method, removing redundant triggers.Gravatar Clément Pit--Claudel2015-08-20
* Move indentation of error messages to the ConsoleErrorReporterGravatar Clément Pit--Claudel2015-08-20
* Simplify error reporting in the trigger generator to get cleaner messagesGravatar Clément Pit--Claudel2015-08-20
* Allow users to disable quantifier splitting by with a {:split false} attributeGravatar Clément Pit--Claudel2015-08-20
* Print matches for triggers as they appear in the bufferGravatar Clément Pit--Claudel2015-08-19
* Enable unicode output in the VS extensionGravatar Clément Pit--Claudel2015-08-19
* Collect ApplyExpr nodes when looking for trigger candidatesGravatar Clément Pit--Claudel2015-08-19
* Fix the equality test for literal expressionsGravatar Clément Pit--Claudel2015-08-19
* Generate triggers for nested quantifiers as wellGravatar Clément Pit--Claudel2015-08-19
* Slightly improve the condition used to filter out trigger setsGravatar Clément Pit--Claudel2015-08-18
* Use nested tokens in the quantifier splitterGravatar Clément Pit--Claudel2015-08-18
* Cleanup indentation of trigger warningsGravatar Clément Pit--Claudel2015-08-19
* Small cleanups, fixes, and refactoringsGravatar Clément Pit--Claudel2015-08-18
* Use a nice warning symbol in some warning messagesGravatar 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 13:37:27 +0000