| Commit message (Expand) | Author | Age |
|---|
| * | Merge |  Rustan Leino | 2014-01-11 |
| |\ |
|
| | * | A better fix to deal with StaticReceiverTypes affected by autoReq. |  Bryan Parno | 2014-01-10 |
| * | | Merge | Rustan Leino | 2014-01-10 |
| |\| |
|
| * | | GHC-MergeSort: removed lemmas and proof steps rendered unnecessary now that a... | Rustan Leino | 2014-01-09 |
| | * | Merge | Bryan Parno | 2014-01-09 |
| | |\
| |/
|/| |
|
| | * | Fixed a resolve bug for UserDefinedTypes | Bryan Parno | 2014-01-09 |
| * | | Dafny renditions of sorting algorithms proved in other provers (Coq, Isabelle... | Rustan Leino | 2014-01-08 |
| |/ |
|
| * | Manually adjusted merge | Rustan Leino | 2014-01-08 |
| * | Merge | Rustan Leino | 2014-01-08 |
| |\ |
|
| * | | Allow left-hand sides of a let expression to be patterns (like in the case of... | Rustan Leino | 2014-01-08 |
| | * | Fixed build break: two contract problems | Rustan Leino | 2014-01-08 |
| | * | :autoReq now works with static functions. | Bryan Parno | 2014-01-08 |
| | * | Add autoReq support for matches. | Bryan Parno | 2014-01-08 |
| | * | Added support for automatic generation of function requirements via the :auto... | Bryan Parno | 2014-01-08 |
| | * | Don't produce default decreases clause for co-predicates, since co-predicates... | Rustan Leino | 2014-01-07 |
| | * | One more file to go with the previous check-in (DafnyRuntime.cs apparently ge... | Rustan Leino | 2014-01-06 |
| | * | Compile assign-such-that for all integers, not just ones where a bound is found | Rustan Leino | 2014-01-06 |
| |/ |
|
| * | More thoroughly check for nested assume statements during compilation | Rustan Leino | 2014-01-05 |
| * | Added ghost let expressions. | Rustan Leino | 2014-01-05 |
| * | Renamed a constructor in a test file | Rustan Leino | 2014-01-03 |
| * | Improved the name-clashing situation when substituting to produce printable A... | Rustan Leino | 2014-01-03 |
| * | Removed unused declaration | Rustan Leino | 2014-01-03 |
| * | Merge | Rustan Leino | 2014-01-03 |
| |\ |
|
| * | | Changed BreadthFirstSearch example to no longer use "inductive naturals", seq... | Rustan Leino | 2014-01-03 |
| | * | Make ModuleDefinition inherit from TopLevelDecl instead of just Declaration | Bryan Parno | 2014-01-03 |
| * | | Allow "match" expressions anywhere | Rustan Leino | 2014-01-03 |
| * | | No longer specialize axioms Haskell-style for functions whose bodies contains... | Rustan Leino | 2014-01-03 |
| * | | Print and translate "match" expressions in general positions, not just at the... | Rustan Leino | 2014-01-03 |
| * | | Embellished axioms about GenericAlloc and DtAlloc. | Rustan Leino | 2014-01-03 |
| |/ |
|
| * | Hover text for inferred postconditions of 'forall' statements (the one for ca... | Rustan Leino | 2013-12-30 |
| * | Merge | Rustan Leino | 2013-12-30 |
| |\ |
|
| * | | Added proper parsing for StmtExpr's in all contexts. | Rustan Leino | 2013-12-30 |
| | * | Pass on attributes for methods, iterators, and functions to Boogie. | wuestholz | 2013-12-26 |
| | * | DafnyExtension: Reduce the default number of Z3 instances by one. | wuestholz | 2013-12-26 |
| | * | Changed the iterator class hover text back to the iterator name (which is con... | Rustan Leino | 2013-12-20 |
| |/ |
|
| * | Hover text for default decreases clauses of loops. | Rustan Leino | 2013-12-20 |
| * | Moved the hover text of iterator classes to the "iterator" keyword itself (si... | Rustan Leino | 2013-12-19 |
| * | Merge | Rustan Leino | 2013-12-19 |
| |\ |
|
| * | | Added an .EndTok for every statement. (Note, in some places, especially in V... | Rustan Leino | 2013-12-19 |
| | * | Merge | Rustan Leino | 2013-12-19 |
| | |\ |
|
| | * | | Compute default decreases clauses in Resolver instead of in the Translator. | Rustan Leino | 2013-12-19 |
| |/ / |
|
| | * | Add pretty-printing flag to the dafny3 test script. | wuestholz | 2013-12-19 |
| |/ |
|
| * | Added test3/GenericSort.dfy, which shows how modules can be used to write and... | Rustan Leino | 2013-12-18 |
| * | Add an assertion to a test case to make it less flaky (hopefully). | wuestholz | 2013-12-18 |
| * | Added missing file (sorry) | Rustan Leino | 2013-12-18 |
| * | Add support for the /verifySeparately flag in Boogie and change most tests to... | wuestholz | 2013-12-18 |
| * | Fix a possible null dereference. | wuestholz | 2013-12-18 |
| * | Fixed pretty printing of calc statements to use the new(-since-long) format. | Rustan Leino | 2013-12-17 |
| * | Don't expand {:opaque} for inherited functions. (Note, more design is still ... | Rustan Leino | 2013-12-17 |
| * | Merge | Rustan Leino | 2013-12-17 |
| |\ |
|
Rustan Leino
Bryan Parno