debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	Removed specContextOnly parameter from ResolveStatement.	leino	2015-09-28
\| \| \| \|	Moved all bounds discovery to resolution pass 1.
*	Type parameters in method/function signatures are no longer auto-declared. ↵	Rustan Leino	2015-07-02
\| \| \| \| \| \| \| \| \| \| \| \| \|	Although convenient and concise, the auto-declare behavior has on many occasions caused confusion when a type name has accidentally been mistyped (and Dafny had then accepted and auto-declared the name). Note, the behavior of filling in missing type parameters is still supported. This mode, although unusual (even original?) in languages, is different from the auto- declare behavior. For auto-declare, identifiers could be used in the program without having a declaration. For fill-in parameters, the implicitly declared type parameters remain anonymous.
*	Improved generation of .reads axioms (correcting an incorrect answer and ↵	leino	2015-05-01
\| \| \| \|	corresponding incorrectly recorded desired answer)
*	Improved encoding of a property of reads clauses to make things more easily ↵	leino	2015-05-01
\| \| \| \|	provable.
*	Refactor resolver, and really allow reads to take fields of type A -> set<obj>	Dan Rosén	2014-08-15
\| \| \| \|	twoState and codeContext is moved to a new class ResolveOpts
*	Compile lambda functions and apply expressions, and change let expr compilation	Dan Rosén	2014-08-12
\|
*	Add higher-order-functions and some other goodies	Dan Rosén	2014-08-11
	* The reads clause now needs to be self framing. * The requires clause now needs to be framed by the reads clause. * There are one-shot lambdas, with a single arrow, but they will probably be removed. * There is a {:heapQuantifier} attribute to quantifiers, but they will probably be removed. * Add smart handling of type variables * Add < and > for datatype & type parameter