debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	Made /rewriteFocalPredicates:1 the default	Rustan Leino	2015-10-02
\|
*	Hover text includes #[_k-1] suffix for terms rewritten in prefix ↵	Rustan Leino	2015-10-02
\| \| \| \| \| \| \|	predicates/lemmas (this fixes an item from the wishlist). Include in hover text the extreme predicates for which an extreme lemmas has been rewritten (but don't include ==# in this list--or should it perhaps be included?). Under a (temporary) switch /rewriteFocalPredicates, each use of a focal predicate P in a prefix lemma is rewritten into P#[_k-1].
*	Stop pretty-print from emitting deprecated semi-colons.	qunyanm	2015-03-05
\|
*	Set up the same test infrastructure as in Boogie.	wuestholz	2014-05-29
\|
*	Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" ↵	Rustan Leino	2014-02-23
\| \| \| \|	-> "prefix lemma")
*	Fixed the problem with the previous check-in.	Rustan Leino	2013-01-18
\|
*	Removed the syntactic form copredicate #-form with the implicit argument.	Rustan Leino	2013-01-16
\| \| \| \|	Added syntactic support for codatatype #-form equalities.
*	Support for copredicates and prefix predicates in comethods.	Rustan Leino	2012-12-04
\| \| \| \| \| \|	(Missing from the co support are (prefix) equalities of codatatypes, various restrictions on the use of co/prefix-predicates, and tactic support for applying the (prefix-)induction automatically.)
*	Change the encoding of proof certificates to make the two levels explicit	Unknown	2012-10-12
\| \| \| \|	Restrict what conclusions comethods are allowed to have
*	New feature:	Rustan Leino	2012-10-11
	* Added "comethod" declarations and support for writing manual co-inductive proofs (but currently blindly assume comethod postconditions to, in positive positions, only have copredicates and codatatype equalities--other cases still need to be dealt with) Code restructuring: * New set of Boogie procedure stubs generated for each other * Start of improvements around TrSplitExpr