| Commit message (Expand) | Author | Age |
* | Fix issue 101. Instead of swapping operands for Exp opcode in BinaryExpr, | qunyanm | 2015-11-10 |
* | Fix issue 99. When annotate a quantifier expr that has a SplitQuantifier, we | qunyanm | 2015-11-06 |
* | Fix issue 104. Use ResolvedExpression to compute subexpressions for | qunyanm | 2015-11-04 |
* | Fix issue89. Copy the out param to a local before use it in an anonymous | qunyanm | 2015-11-04 |
* | Fix issue 91 - Change how we compute the bounds of quantified variables so that | qunyanm | 2015-10-29 |
* | 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 Ru... | wuestholz | 2015-10-26 |
|/ |
|
* | Make /autoTriggers:1 be the default in Visual Studio | leino | 2015-10-24 |
* | In Visual Studio, be willing to display both resolution warnings and verifica... | leino | 2015-10-24 |
* | 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 |
* | 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 its... | Bryan Parno | 2015-10-19 |
* | Version 1.9.6.21012 | 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 |
* | 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 |
* | Fixed latent crash of hovertext/outlining with include. | Rustan Leino | 2015-10-02 |
* | Removed some unused code. | Rustan Leino | 2015-09-30 |
* | Merge | leino | 2015-09-29 |
|\ |
|
| * | Fix the build. | wuestholz | 2015-09-29 |
* | | Merge | leino | 2015-09-28 |
|\| |
|
* | | Removed specContextOnly parameter from ResolveStatement. | leino | 2015-09-28 |
* | | Removed the 'inSpecOnlyContext' map that had been part of the resolution of | leino | 2015-09-28 |
* | | Renamed CheckIsNonGhost to CheckIsCompilable. | leino | 2015-09-28 |
* | | Removed more traces of the previous resolution checks that happened during pa... | leino | 2015-09-28 |
* | | Changed computation of ghosts until pass 2 of resolution. | leino | 2015-09-28 |
| * | fixed bugs related to identifying newtypes as types of integers and reals. | Michael Lowell Roberts | 2015-09-23 |
| * | fix for warnings related to deprecated z3 options (please update to the lates... | Michael Lowell Roberts | 2015-09-22 |
* | | Removed unused code (old code from previous ghost-statement handling) | leino | 2015-09-21 |
* | | Moved premature uses of .IsGhost for Statement's | leino | 2015-09-21 |
| * | Auto-merged heads. | Michael Lowell Roberts | 2015-09-21 |
| |\ |
|
| * | | merged IronDafny updates. two unit tests related to traits do not pass if ENA... | Michael Lowell Roberts | 2015-09-21 |
* | | | Preliminary refactoring of ghost-statement computations to after type checking | leino | 2015-09-20 |
| | * | Fix a check that occasionally led to an out of bounds exception in the extension | Bryan Parno | 2015-09-17 |
| * | | Only print extraneous comments if asked. | Michael Lowell Roberts | 2015-09-17 |
| |/ |
|
* | | Merge | leino | 2015-09-11 |
|\| |
|
* | | Refactored most of UnifyTypes calls into a ConstrainTypes method, preparing f... | leino | 2015-08-31 |
| * | Align the server's default kill time with the one of the VS extension | Clément Pit--Claudel | 2015-08-28 |
| * | Implement {:nowarn}, clarify some messages, and add a few tests | Clément Pit--Claudel | 2015-08-28 |
|/ |
|
* | Tiny cleanup in TriggersCollector | Clément Pit--Claudel | 2015-08-27 |
* | Look for z3 in Binaries/z3/bin (but keep the vendored version for convenience) | Clément Pit--Claudel | 2015-08-27 |
* | Further relax the loop detection conditions | Clément Pit--Claudel | 2015-08-27 |
* | Small fix: there is no loop in (forall x :: Q(x) && Q(0)) | Clément Pit--Claudel | 2015-08-27 |