debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	In the VS IDE, don't generate hover-text information for auto-generated ↵	leino	2015-11-05
\| \| \| \|	identifiers
*	Fixed latent crash of hovertext/outlining with include.	Rustan Leino	2015-10-02
\| \| \| \|	(This also undoes two previous attempted fixes, which had accidentally disabled some outlining and hovertexts.)
*	Fix a check that occasionally led to an out of bounds exception in the extension	Bryan Parno	2015-09-17
\|
*	Discard error messages that refer to a non-nested TokenWrapper.	Clément Pit--Claudel	2015-08-20
\| \| \| \| \| \| \| \|	The VS extension already did that, but it also filtered out nested tokens. That prevented info about triggers from being reported. Other interfaces (the CLI and Emacs, in particular) should have the same ability. Surprinsingly, this doesn't cause any tests failures.
*	Refactor the error reporting code	Clément Pit--Claudel	2015-08-18
\| \| \| \| \|	The new error reporting system has a simpler interface, isn't tied to the resolver, and contains error source information.
*	Fix identifiers in nested match patterns not showing in the IDE bug. Remember	qunyanm	2015-06-29
\| \| \| \| \|	BoundVars that are combined in rewriting of the nested match patterns so they show up in the IDE correctly.
*	Added {:auto_generated} trigger, which indicates that a declaration was not ↵	Rustan Leino	2015-06-02
\| \| \| \|	explicitly mentioned in the input. This lets the Dafny IDE know not to add hovertext for these declarations.
*	Various resolution fixes and improvements	leino	2014-08-26
\| \| \| \| \|	Added IsGoodHeap antecedent in (exists heap ...) in newtype Is axioms. Added IDE tool tips in newtype constraints.
*	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
*	Refactoring: renamed VarDecl to LocalVariable, and renamed VarDeclStmt.Lhss ↵	Rustan Leino	2014-03-17
\| \| \| \|	to VarDeclStmt.Locals
*	Fixed bug in DafnyExtension (hover text computation would crash if ↵	Rustan Leino	2014-02-06
\| \| \| \| \| \|	Translator had not been run). Fixed duplicate hover text information for Lines of calc statements.
*	Mark auto-generated expressions (in "decreases" clauses) and don't use these ↵	Rustan Leino	2014-02-04
\| \| \| \|	when figuring out hover text.
*	Manually adjusted merge	Rustan Leino	2014-01-08
\|
*	Compute default decreases clauses in Resolver instead of in the Translator.	Rustan Leino	2013-12-19
\| \| \| \|	Make this information available as AdditionalInformation, that is, as hover text in the IDE.
*	DafnyExtension: Added support for displaying values from the model as hover ↵	wuestholz	2013-07-30
\| \| \| \|	text.
*	DafnyExtension: Added support for selecting errors and showing the model in BVD.	wuestholz	2013-07-15
\|
*	DafnyExtension: Added support for collecting additional information during ↵	wuestholz	2013-07-15
\| \| \| \|	resolution and displaying it.
*	DafnyExtension: Made it display verification errors incrementally.	wuestholz	2013-06-20
\|
*	DafnyExtension: Did some refactoring.	wuestholz	2013-06-11
\|
*	In Visual Studio interface, highlight variable definitions of let expressions	Rustan Leino	2013-05-12
\|
*	Renamed "parallel" statement to "forall" statement, and made the parentheses ↵	Rustan Leino	2013-03-06
\| \| \| \|	around the bound variables optional.
*	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.)
*	Improved Dafny Extension display of destructors	Rustan Leino	2012-11-19
\|
*	Rename _reverifyPost to $_reverifyPost, so that it doesn't show up in BVD	Rustan Leino	2012-10-30
\| \| \| \| \|	Remove some duplicated hover text in DafnyExtension Enable Code Contracts in the build
*	Hover text for iterator declarations (and not for the methods they generate)	Rustan Leino	2012-10-04
\|
*	More free antecedents when proving well-formedness of iterator specs	Rustan Leino	2012-10-04
\|
*	Put all sources under \Source directory	Rustan Leino	2012-10-04