summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
* MergeGravatar Clément Pit--Claudel2015-08-21
|\
* | 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
* | Adjust WF checks to use unsplit quantifiers.Gravatar Clément Pit--Claudel2015-08-21
* | Add some diversity to Dafny's alimentationGravatar Clément Pit--Claudel2015-08-21
* | Give up on trying to set the console's input encoding to UTF8Gravatar 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
| * MergeGravatar Rustan Leino2015-08-20
| |\ | |/ |/|
| * Changed equality tests involving traits from using strings to using reference...Gravatar Rustan Leino2015-08-20
| * Minor refactoringGravatar Rustan Leino2015-08-20
| * Fixed compilation that involve enumeration over native-type newtype values.Gravatar Rustan Leino2015-08-20
* | Make the dependency that DafnyServer has on DafnyPipeline explicitGravatar Clément Pit--Claudel2015-08-20
* | Implement the SelectTrigger method, removing redundant triggers.Gravatar Clément Pit--Claudel2015-08-20
* | Merge.Gravatar Clément Pit--Claudel2015-08-20
|\|
* | Move indentation of error messages to the ConsoleErrorReporterGravatar Clément Pit--Claudel2015-08-20
* | Discard error messages that refer to a non-nested TokenWrapper.Gravatar Clément Pit--Claudel2015-08-20
| * Fixed bug in type unificationGravatar Rustan Leino2015-08-20
| * MergeGravatar Rustan Leino2015-08-20
| |\
* | | Simplify error reporting in the trigger generator to get cleaner messagesGravatar Clément Pit--Claudel2015-08-20
* | | Mark a few reporting functions as staticGravatar 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
* | | Add a check for SplitQuantifiers that had been incorrectly left out from the ...Gravatar Clément Pit--Claudel2015-08-19
* | | Factor out some AST visiting codeGravatar Clément Pit--Claudel2015-08-19
| |/ |/|
| * Refactored and improved bounds discoveryGravatar Rustan Leino2015-08-19
* | Use /tracePO instead of /trace in the serverGravatar Clément Pit--Claudel2015-08-19
* | Enable unicode output in the VS extensionGravatar Clément Pit--Claudel2015-08-19
* | server: always print tooltipsGravatar 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
* | Merge.Gravatar Clément Pit--Claudel2015-08-19
|\|
* | Server: disable tracing when running tests, and fix an encoding issue.Gravatar Clément Pit--Claudel2015-08-18
* | Slightly improve the condition used to filter out trigger setsGravatar Clément Pit--Claudel2015-08-18
* | Check Reads and Decreases clauses for expressions that could prevent inliningGravatar Clément Pit--Claudel2015-08-18
* | Refactor calls to 'new CallCmd' and clear a few FIXMEsGravatar 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
| * Changed hover-text location for recursive ind/co-lemma callsGravatar Rustan Leino2015-08-17
| * Update the way bounds are discovered to try to choose "better" bounds.Gravatar Bryan Parno2015-08-17
* | Review preceding commit with RustanGravatar Clément Pit--Claudel2015-08-17
* | Start committing split quantifiersGravatar Clément Pit--Claudel2015-08-14
* | Implement self-loop detectionGravatar Clément Pit--Claudel2015-08-14
* | Start committing generated triggers when /autoTriggers is 1Gravatar Clément Pit--Claudel2015-08-14
* | Run the trigger rewriter after the quantifier splitterGravatar Clément Pit--Claudel2015-08-14
* | Draft out a more advanced version of trigger generationGravatar Clément Pit--Claudel2015-08-19
* | Refactor the error reporting codeGravatar Clément Pit--Claudel2015-08-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-07 19:44:02 +0000