debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	Make /autoTriggers:1 to be default. Add /autoTriggers:0 to tests that requires	qunyanm	2016-03-28
\| \| \| \| \|	it. Don't use pretty warning signs since we can't diff them correctly in the test output from the test run.
*	Mark old "import A as B" syntax as deprecated. The new syntax is "import A : B"	qunyanm	2016-02-02
\|
*	Fixed compilation of equality between reference types	leino	2015-11-11
\|
*	Implemented resolution, verification, and (poorly performing) compilation of ↵	leino	2015-10-05
\| \| \| \| \| \| \|	existential if guards. Fixed bugs in ghost checks involving comprehensions and attributes. Added SubstituteBoundedPool method.
*	Stop pretty-print from emitting deprecated semi-colons.	qunyanm	2015-03-05
\|
*	Language change: All functions and methods declared lexically outside any ↵	leino	2014-12-12
\| \| \| \| \| \| \| \| \| \|	class are now automatically static, and fields are no longer allowed to be declared there. Stated differently, all heap state must now be declared inside an explicitly declared class, and functions and methods declared outside any class can be viewed as belonging to the module. The motivating benefit of this change is to no longer need the 'static' keyword when declaring a module of functions and methods.
*	Allow underscores in numeric literals (and in field/destructor names that ↵	leino	2014-10-23
\| \| \| \| \| \|	are written as numeric strings). The underscores have no semantic meaning, but can help a human parse the numbers.
*	Set up the same test infrastructure as in Boogie.	wuestholz	2014-05-29
\|
*	Added ghost let expressions.	Rustan Leino	2014-01-05
\|
*	Add support for the :axiom attribute for ghost methods.	Bryan Parno	2013-12-13
\| \| \| \| \| \|	This suppresses compiler errors for ghost methods and functions without bodies. Also changed the parser to complain about bodyless methods and functions without bodies if /noCheating:1 is specified.
*	Allow field names to be sequences of digits (this is nice, for example, to ↵	Rustan Leino	2013-07-24
\| \| \| \|	define a Tuple with fields .0 and .1)
*	Fixed compilation bug where C# keywords were not being escaped	Rustan Leino	2013-06-25
\|
*	renamed "abstract module" to "module facade"	Rustan Leino	2012-10-22
\| \| \| \|	renamed "ghost module" to "abstract module", adding a keyword "abstract"
*	Dafny: updated test suite to new syntax	Jason Koenig	2012-07-30
\|
*	Dafny: compilation of abstract modules, including local definitions (as in ↵	Jason Koenig	2012-07-17
\| \| \| \| \| \| \|	module A as B = C) * * * Dafny: compilation of abstract modules, including local definitions (as in module A as B = C)
*	Dafny: added support for co-recursive calls	Rustan Leino	2012-05-01
\|
*	Dafny: fixed resolution bug for inductive datatypes (previous check did not ↵	Unknown	2012-04-25
	handle generic datatypes correctly) Dafny: fixed compiler bug in inductive datatypes (missing type parameters in emitted code) Dafny: added "codatatype" declaration (syntax only for now)