debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	Fix issue 103. Emit the quantifiers for ForallStmt before AutoTrigger so that	qunyanm	2015-11-25
\| \| \| \|	the auto-triggers can be computed for ForallStmt.
*	Add code that uses Z3's optimization features (currently disabled by default).	wuestholz	2015-11-19
\|
*	Fix issue 108. Use idGenerator to create a new collection name for each	qunyanm	2015-11-18
\| \| \| \|	occurrence of Set/MapComprehension when translating it to c#.
*	Changed checked-in version of Z3 to 4.4.1 (from 4.4.0)	leino	2015-11-17
\|
*	Fix issue 107. Instead of writing out StaticReceiverExpr as null valued	qunyanm	2015-11-17
\| \| \| \|	LiteralExpr, write out its type instead.
*	Fix issue 100. Add an axiom for functionHandle to trigger off of the origial	qunyanm	2015-11-17
\| \| \| \|	function and connect with Apply1 of the function.
*	Updated version number to 1.9.6.21116. This version is now on rise4fun.	leino	2015-11-16
\|
*	Fix issue 94. Allow tuple-based assignment in statement contexts.	qunyanm	2015-11-14
\|
*	Merge	leino	2015-11-11
\|\
* \|	Fixed compilation of equality between reference types	leino	2015-11-11
\| \|
\| *	Fix issue 101. Instead of swapping operands for Exp opcode in BinaryExpr,	qunyanm	2015-11-10
\| \| \| \| \| \| \| \| \| \|	swap them when the expr is first created in parser or for calcstmt. This avoids problems of operands being swapped again when the expr is copied.
\| *	Fix issue 99. When annotate a quantifier expr that has a SplitQuantifier, we	qunyanm	2015-11-06
\| \| \| \| \| \| \| \| \| \|	need exclude the private terms (the ones that includes the quantifier expr's bv) from it exported terms.
* \|	Merge	leino	2015-11-06
\|\\|
* \|	Updated syntax of test case to remove unnecessary semicolons and parentheses	leino	2015-11-05
\| \|
* \|	In the VS IDE, don't generate hover-text information for auto-generated ↵	leino	2015-11-05
\| \| \| \| \| \| \| \|	identifiers
\| *	Fix issue 104. Use ResolvedExpression to compute subexpressions for	qunyanm	2015-11-04
\| \| \| \| \| \| \| \|	DatatypeUpdateExpr if ResovedExpression is not null.
\| *	Fix issue89. Copy the out param to a local before use it in an anonymous	qunyanm	2015-11-04
\| \| \| \| \| \| \| \| \| \| \| \|	method that is generated by LetExpr. Change the compiler so that each stmt writes to its own buffer before add it to the program's buffer so that we can insert the above mentioned copy instruction before the stmt.
\| *	Add some files to .hgignore.	wuestholz	2015-11-02
\| \|
\| *	update the test.	qunyanm	2015-10-30
\| \|
\| *	Fix issue 91 - Change how we compute the bounds of quantified variables so that	qunyanm	2015-10-29
\| \| \| \| \| \| \| \|	it does not depend on the order they appeared.
\| *	Check version info before delete white space so that it will work with python	qunyanm	2015-10-28
\|/ \| \| \|	version that is less than 3.
*	Merge	leino	2015-10-26
\|\
* \|	Fixed location of blue dots to appear after semi-colons, not just before them.	leino	2015-10-26
\| \|
\| *	DafnyExtension: Add menu item for automatic induction (mainly developed by ↵	wuestholz	2015-10-26
\|/ \| \| \|	Rustan).
*	Make /autoTriggers:1 be the default in Visual Studio	leino	2015-10-24
\|
*	In Visual Studio, be willing to display both resolution warnings and ↵	leino	2015-10-24
\| \| \| \| \| \|	verification errors (previously, verification errors were masked by resolution warnings)
*	In method and iterator specifications, inline top-level predicates (except	leino	2015-10-24
\| \| \| \|	protected predicated in cross-module calls) like in other places.
*	Introduced new datatype update syntax: D.(f := E)	leino	2015-10-23
\| \| \| \| \|	The old syntax, D[f := E], is still supported for a short while, but generates a warning about that syntax being deprecated. The new syntax also supports multiple updates: D.(f := E0, g := E1, h := E2)
*	Refactored resolution of datatype updates, preparing for a change of syntax	leino	2015-10-23
\|
*	Fixed bug introduced in changeset 7ebdf9cd4154	leino	2015-10-22
\|
*	Improve Dafny's ability to find fueled functions by checking the function ↵	Bryan Parno	2015-10-19
\| \| \| \| \| \|	itself, as well as the signature and body of other functions.
*	Version 1.9.6.21012	Rustan Leino	2015-10-12
\|
*	Merge	Rustan Leino	2015-10-12
\|\
\| *	DafnyExtension: Re-added assembly reference.	wuestholz	2015-10-08
\| \|
\| *	DafnyExtension: Fix concurrency issue.	wuestholz	2015-10-08
\| \|
\| *	Make the Dafny extension compile on VS 2015 without any old versions.	wuestholz	2015-10-08
\| \|
\| *	Add vsix to releases and fix invalid path separators in packaging script	Clément Pit--Claudel	2015-10-08
\| \|
* \|	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
\| \| \| \| \| \| \|	existential if guards. Fixed bugs in ghost checks involving comprehensions and attributes. Added SubstituteBoundedPool method.
*	Parsing and pretty printing of the new "existential guards" of the two kinds ↵	leino	2015-10-03
\| \| \| \|	of "if" statements.
*	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].
*	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.)
*	Removed some unused code.	Rustan Leino	2015-09-30
\|
*	Merge	leino	2015-09-29
\|\
\| *	Fix two test cases that failed if the path to "DafnySever.exe" contained spaces.	wuestholz	2015-09-30
\| \|
\| *	Fix the build.	wuestholz	2015-09-29
\| \|
* \|	Merge	leino	2015-09-28
\|\ \
\| * \|	Merge	leino	2015-09-28
\| \|\\|