| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Add an infinite set collection type. |  qunyanm | 2015-05-29 |
| | | |||
| * | Added 'protected' keyword (syntax) | leino | 2015-03-07 |
| | | |||
| * | Add imap keyword to VS/emacs/vim/latex files | chrishaw | 2015-02-26 |
| | | |||
| * | Added types "char" and "string" (the latter being a synonym for "seq<char>"). | leino | 2014-10-20 |
| | | | | | | | Added string literals with various escapes--a subset of those supported in C# and similar languages, including the C# verbatim strings. Previously, the "print" statement and custom attributes could support expression-or-string arguments; there is no longer a need to special-case these, so these arguments are now just expressions. Fixed lack of operator resolution in custom attributes. | ||
| * | Changed syntax of derived types to "newtype" | leino | 2014-08-21 |
| | | | | | Added parsing of constraints (beyond parsing is yet to come) | ||
| * | added trait feature: |  Reza Ahmadi | 2014-07-18 |
| | | | | | | | -possibility to declare traits in Dafny -possibility to extend a class by a trait -possibility to override body-less methods | ||
| * | Fixes to vim highlighting |  Dan Rosén | 2014-07-07 |
| | | |||
| * | Added "modify" statement. | Rustan Leino | 2014-04-03 |
| | | | | | In a frame govered by a ghost context, ignore explicit mentions of `g if g is a ghost field. | ||
| * | Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" ↵ | Rustan Leino | 2014-02-23 |
| | | | | | -> "prefix lemma") | ||
| * | Syntax highlighting for reals | Rustan Leino | 2014-02-13 |
| | | |||
| * | Add support for the "include" keyword, which accepts a (possibly relative) path |  Bryan Parno | 2013-12-10 |
| | | | | | | to another Dafny file. That file's functions and methods are included but not checked. This is intended to support incremental verification on a per-file basis. | ||
| * | Removed old keyword "choose" | Rustan Leino | 2013-08-06 |
| | | |||
| * | Introduced keywords "lemma" (like a "ghost method", but not allowed to have ↵ | Rustan Leino | 2013-08-02 |
| | | | | | a "modifies" clause) and "colemma" (synonymous with "comethod"; perhaps "comethod" will go away at some point) | ||
| * | Renamed "parallel" statement to "forall" statement, and made the parentheses ↵ | Rustan Leino | 2013-03-06 |
| | | | | | around the bound variables optional. | ||
| * | removed deprecated "allocated" keyword from DafnyExtension syntax highlighting |  Rustan Leino | 2012-10-22 |
| removed a level of directories for the Dafny VIM mode | |||
 |
index : debian-dafny | |
| Debian packaging for Dafny |
| summaryrefslogtreecommitdiff |