| Commit message (Expand) | Author | Age |
* | 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 |
|\ |
|
* | | Don't inline opaque functions. | Rustan Leino | 2013-12-17 |
| * | Merge | Rustan Leino | 2013-12-16 |
| |\
| |/
|/| |
|