summaryrefslogtreecommitdiff
path: root/Source/Dafny/Triggers/QuantifiersCollection.cs
Commit message (Expand)AuthorAge
* Implement {:nowarn}, clarify some messages, and add a few testsGravatar Clément Pit--Claudel2015-08-28
* 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
* Add a sanity check in QuantifiersCollectionGravatar Clément Pit--Claudel2015-08-23
* Rephrase the message about triggers being rejected because they are too strongGravatar 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
* 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
* Slightly improve the condition used to filter out trigger setsGravatar 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
* 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-05-14 20:29:30 +0000