| Commit message (Expand) | Author | Age |
* | Added ghost let expressions. | Rustan Leino | 2014-01-05 |
* | Improved the name-clashing situation when substituting to produce printable A... | Rustan Leino | 2014-01-03 |
* | Merge | 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 |
|/ |
|
* | 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 |
| * | Compute default decreases clauses in Resolver instead of in the Translator. | Rustan Leino | 2013-12-19 |
|/ |
|
* | 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 |
| |\
| |/
|/| |
|
| * | Fixed bug where free conditions preceded checked conditions (for inlined pred... | Rustan Leino | 2013-12-16 |
* | | Pass assert/assume attributes down to Boogie | Rustan Leino | 2013-12-16 |
* | | Fix build failure due to changes in Boogie. | wuestholz | 2013-12-16 |
* | | Merge | Bryan Parno | 2013-12-13 |
|\ \ |
|
* | | | Add support for the :axiom attribute for ghost methods. | Bryan Parno | 2013-12-13 |
| * | | Produce "tail recursive" hover text in the IDE only for methods that are recu... | Rustan Leino | 2013-12-13 |
* | | | Added support for opaque function definitions, indicated via the {:opaque} at... | Bryan Parno | 2013-12-13 |
|/ / |
|
* | | Add a command-line option to disable include directives. | Bryan Parno | 2013-12-13 |
* | | Merge | Rustan Leino | 2013-12-11 |
|\ \ |
|
* | | | Refactored the calling of rewriters | Rustan Leino | 2013-12-11 |
| * | | Fix build failures due to changes in Boogie. | wuestholz | 2013-12-11 |
| * | | Add support for the "include" keyword, which accepts a (possibly relative) path | Bryan Parno | 2013-12-10 |
|/ / |
|
* | | Fixed a bug in the Boogie generated for refinement checks (now that there is ... | Rustan Leino | 2013-12-09 |
* | | Fixed bug reported as discussion:472216 on dafny.codeplex.com | Rustan Leino | 2013-12-09 |
* | | Fix some things due to changes in Boogie (execution engine API, 'UnivBackPred... | wuestholz | 2013-12-09 |
* | | Fixed build failures due to changes in Boogie. | wuestholz | 2013-11-23 |
|/ |
|
* | Use full name of type in compilation error | Rustan Leino | 2013-11-18 |
* | Merge | Rustan Leino | 2013-11-18 |
|\ |
|
| * | Added support for attributes on variable declarations. | wuestholz | 2013-11-18 |
* | | Let compiler complain about body-less functions and methods, even if these ar... | Rustan Leino | 2013-11-14 |
|/ |
|
* | Fixed build failure due to changes in Boogie. | wuestholz | 2013-10-28 |
* | Removed old keyword "choose" | Rustan Leino | 2013-08-06 |
* | Bumped version to 1.7.0, to be released as a binary and on rise4fun. | wuestholz | 2013-08-06 |
* | Removed code for an unreachable case | Rustan Leino | 2013-08-06 |
* | Merge | Rustan Leino | 2013-08-06 |
|\ |
|