debian-dafny - Debian packaging for Dafny

	Commit message (Expand)	Author	Age
*	Fix issue 103. Emit the quantifiers for ForallStmt before AutoTrigger so that	qunyanm	2015-11-25
*	Fixed compilation of equality between reference types	leino	2015-11-11
*	Fix issue 91 - Change how we compute the bounds of quantified variables so that	qunyanm	2015-10-29
*	In method and iterator specifications, inline top-level predicates (except	leino	2015-10-24
*	Introduced new datatype update syntax: D.(f := E)	leino	2015-10-23
*	Improve Dafny's ability to find fueled functions by checking the function its...	Bryan Parno	2015-10-19
*	Renamed ExistentialGuards... to BindingGuards...	Rustan Leino	2015-10-07
*	Use /env:0 to avoid full pathnames in test output	Rustan Leino	2015-10-06
*	Implemented resolution, verification, and (poorly performing) compilation of ...	leino	2015-10-05
*	Parsing and pretty printing of the new "existential guards" of the two kinds ...	leino	2015-10-03
*	Made /rewriteFocalPredicates:1 the default	Rustan Leino	2015-10-02
*	Hover text includes #[_k-1] suffix for terms rewritten in prefix predicates/l...	Rustan Leino	2015-10-02
*	Removed specContextOnly parameter from ResolveStatement.	leino	2015-09-28
*	Removed more traces of the previous resolution checks that happened during pa...	leino	2015-09-28
*	Additional tests	leino	2015-09-28
*	Whitespace changes in test file	leino	2015-09-28
*	Changed computation of ghosts until pass 2 of resolution.	leino	2015-09-28
*	Added back in various ghost tests	leino	2015-09-20
*	Changes that only affect line numbers in test case	leino	2015-09-20
*	Removed tabs from test file	leino	2015-09-20
*	Preliminary refactoring of ghost-statement computations to after type checking	leino	2015-09-20
*	Merge	Clément Pit--Claudel	2015-09-02
\|\
* \|	Add a small test from a discussion with Bryan	Clément Pit--Claudel	2015-08-28
* \|	Implement workarounds for some tests that fail with /autoTriggers.	Clément Pit--Claudel	2015-08-28
* \|	Suppress many warnings in the test suite.	Clément Pit--Claudel	2015-08-28
\| *	Added tests for Boogie's new /verifySnapshots:3, which will be used by the Da...	Rustan Leino	2015-08-28
\|/
*	Add change missing from bd47e3cdb79c	Clément Pit--Claudel	2015-08-23
*	Added /autoTriggers to two tests where it only makes a cosmetic difference	Clément Pit--Claudel	2015-08-23
*	Replace b \|\| !b by true in Snapshots5.v1.dfy	Clément Pit--Claudel	2015-08-23
*	Fix: multi-dimensional OOB errors were sometimes reported on incorrect locati...	Clément Pit--Claudel	2015-08-23
*	Merge	Rustan Leino	2015-08-20
\|\
* \|	Fixed compilation that involve enumeration over native-type newtype values.	Rustan Leino	2015-08-20
\| *	Merge.	Clément Pit--Claudel	2015-08-20
\| \|\ \| \|/ \|/\|
* \|	Merge	Rustan Leino	2015-08-20
\|\ \
\| \| *	Add a test to check that there are as many errors as failed preconditions	Clément Pit--Claudel	2015-08-19
\| \|/
* \|	Refactored and improved bounds discovery	Rustan Leino	2015-08-19
\| *	Merge.	Clément Pit--Claudel	2015-08-19
\| \|\ \| \|/ \|/\|
\| *	Cleanup indentation of trigger warnings	Clément Pit--Claudel	2015-08-19
\| *	Draft out a more advanced version of trigger generation	Clément Pit--Claudel	2015-08-19
* \|	Change the induction heuristic for lemmas to also look in precondition for cl...	leino	2015-08-12
\|/
*	Merge	Rustan Leino	2015-07-31
\|\
\| *	Merge	leino	2015-07-31
\| \|\
* \| \|	Bug fix: check that assign-such-that constraint is of type boolean	Rustan Leino	2015-07-31
\| \|/ \|/\|
\| *	Allow forall statements in refinements	leino	2015-07-31
* \|	Add quotes in snapshot tests.	Clément Pit--Claudel	2015-07-30
* \|	Fixed crash in resolution where, after reporting an error, the cases #type an...	Rustan Leino	2015-07-29
* \|	Clarify the inlining warning.	Clément Pit--Claudel	2015-07-27
\|/
*	Fix: Read clauses should be checked before lit lifting	Clément Pit--Claudel	2015-07-23
*	Fix: Unify column numbers in Dafny's errors	Clément Pit--Claudel	2015-07-23
*	Improved rank axioms for containers	Rustan Leino	2015-07-21