index
:
debian-dafny
master
Debian packaging for Dafny
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
...
*
|
Improve error reporting for split quantifiers
Clément Pit--Claudel
2015-08-23
*
|
Allow MultiSelectExpr as quantifier heads
Clément Pit--Claudel
2015-08-23
*
|
Trivial code cleanup
Clément Pit--Claudel
2015-08-23
*
|
Exclude axiom-profiler.html and z3.log files in the Test directory
Clément Pit--Claudel
2015-08-23
*
|
Fix: multi-dimensional OOB errors were sometimes reported on incorrect locati...
Clément Pit--Claudel
2015-08-23
*
|
Ignore .bpl files in the Test directory
Clément Pit--Claudel
2015-08-22
*
|
Add one more wish: it would be nice to be able to prove exists b: bool :: b
Clément Pit--Claudel
2015-08-22
*
|
Grant "wishlist/useless-casts-in-decreases-clauses.dfy"
Clément Pit--Claudel
2015-08-22
*
|
Add more wishes to the wishlist
Clément Pit--Claudel
2015-08-22
*
|
Ignore flycheck_ and .orig files
Clément Pit--Claudel
2015-08-22
*
|
Look at the full quantifier to find loops, not just the term.
Clément Pit--Claudel
2015-08-22
|
/
*
Set exec flag on Binaries/z3
Clément Pit--Claudel
2015-08-22
*
Add a 'tutorial' folder to the distribution, with an initial example.
Clément Pit--Claudel
2015-08-22
*
Merge
Clément Pit--Claudel
2015-08-21
|
\
*
|
Make `old` a special case for trigger generation.
Clément Pit--Claudel
2015-08-21
*
|
Rephrase the message about triggers being rejected because they are too strong
Clément Pit--Claudel
2015-08-21
*
|
Add a few things to the wishlist
Clément Pit--Claudel
2015-08-21
*
|
Adjust WF checks to use unsplit quantifiers.
Clément Pit--Claudel
2015-08-21
*
|
Add some diversity to Dafny's alimentation
Clément Pit--Claudel
2015-08-21
|
*
Make use of new syntax in a test file
Rustan Leino
2015-08-21
*
|
Interleave stderr output with test results; this allows one to print stuff
Clément Pit--Claudel
2015-08-21
*
|
Ignore flycheck_* files in runTests
Clément Pit--Claudel
2015-08-21
*
|
Add tests for display expressions used as triggers
Clément Pit--Claudel
2015-08-21
*
|
Give up on trying to set the console's input encoding to UTF8
Clément Pit--Claudel
2015-08-21
*
|
Allow display expressions as trigger terms
Clément Pit--Claudel
2015-08-21
*
|
Add /printTooltips to trigger tests
Clément Pit--Claudel
2015-08-21
*
|
Cleanup a number of FIXMEs that I had left in the code
Clément Pit--Claudel
2015-08-20
|
*
Merge
Rustan Leino
2015-08-20
|
|
\
|
|
/
|
/
|
|
*
Changed equality tests involving traits from using strings to using reference...
Rustan Leino
2015-08-20
|
*
Minor refactoring
Rustan Leino
2015-08-20
|
*
Fixed compilation that involve enumeration over native-type newtype values.
Rustan Leino
2015-08-20
*
|
Make the dependency that DafnyServer has on DafnyPipeline explicit
Clément Pit--Claudel
2015-08-20
*
|
Fix a typo
Clément Pit--Claudel
2015-08-20
*
|
Implement the SelectTrigger method, removing redundant triggers.
Clément Pit--Claudel
2015-08-20
*
|
Merge.
Clément Pit--Claudel
2015-08-20
|
\
|
*
|
Move indentation of error messages to the ConsoleErrorReporter
Clément Pit--Claudel
2015-08-20
*
|
Discard error messages that refer to a non-nested TokenWrapper.
Clément Pit--Claudel
2015-08-20
|
*
Fixed bug in type unification
Rustan Leino
2015-08-20
|
*
Merge
Rustan Leino
2015-08-20
|
|
\
*
|
|
Add unit tests for trigger-related error messages
Clément Pit--Claudel
2015-08-20
*
|
|
Simplify error reporting in the trigger generator to get cleaner messages
Clément Pit--Claudel
2015-08-20
*
|
|
Mark a few reporting functions as static
Clément Pit--Claudel
2015-08-20
*
|
|
Add a test to show how trigger splitting balances the downsides of loop detec...
Clément Pit--Claudel
2015-08-20
*
|
|
Allow users to disable quantifier splitting by with a {:split false} attribute
Clément Pit--Claudel
2015-08-20
*
|
|
Add a wishlist folder to the test suite, with things that we do not support (...
Clément Pit--Claudel
2015-08-19
*
|
|
Add a test to check that there are as many errors as failed preconditions
Clément Pit--Claudel
2015-08-19
*
|
|
Add tests for quantifier splitting and trigger generation
Clément Pit--Claudel
2015-08-19
*
|
|
Print matches for triggers as they appear in the buffer
Clément Pit--Claudel
2015-08-19
*
|
|
Add a check for SplitQuantifiers that had been incorrectly left out from the ...
Clément Pit--Claudel
2015-08-19
*
|
|
Factor out some AST visiting code
Clément Pit--Claudel
2015-08-19
|
|
/
|
/
|
[prev]
[next]