| Commit message (Expand) | Author | Age |
|---|
| * | Add /view:<view1, view2> option to filter module exports to be printed. |  qunyanm | 2016-02-11 |
| * | Fix issue 131. Instead of crashing, report an error when an undefined member of | qunyanm | 2016-02-09 |
| * | Fix issue 120. Need to wrap operations that are "lit lifted" and turned into | qunyanm | 2016-02-08 |
| * | Fix issue 124. Consider math operators that later turned into function calls | qunyanm | 2016-02-08 |
| * | Fix issue 125. Add the missing case 2 and 3 with refinement and opened imports. | qunyanm | 2016-02-05 |
| * | Fix issue 128. Change the translation of CanCallAssumption for let-such-that | qunyanm | 2016-02-04 |
| * | Fix issue 129. When looking for a constructor for which Dafny knows how to | qunyanm | 2016-02-02 |
| * | Mark old "import A as B" syntax as deprecated. The new syntax is "import A : B" | qunyanm | 2016-02-02 |
| * | Implement module export so we can export a subset of items defined in the | qunyanm | 2016-01-29 |
| * | Revert Makefile to its prior settings |  Richard L. Ford | 2016-01-29 |
| * | Fix build and test failures, cleanup grammar. | Richard L. Ford | 2016-01-27 |
| * | Implement 'extern' declaration modifier. | Richard L. Ford | 2016-01-27 |
| * | Fix issue 121. Don't split QuantifierExpr that are empty. | qunyanm | 2016-01-25 |
| * | Fix issue 122. Only generate autoTriggers for QuantifierExpr that are not | qunyanm | 2016-01-25 |
| * | Mark temps that are generated in the resolver as auto-generated identifiers so | qunyanm | 2016-01-20 |
| * | Fix issue 117. Generate an error when the "opened" of an import doesn't match | qunyanm | 2016-01-08 |
| * | Fix issue 118. When iteratively computing bounds, treat RefBoundedPool typed | qunyanm | 2016-01-07 |
| * | Removed Contract.Requires from method overrides (preconditions of overrides a... | Rustan Leino | 2016-01-06 |
| * | Fix issue 116. Add the missing @ for the generated c# code. | qunyanm | 2016-01-05 |
| * | Fix issue 114. Do not export private terms for ComprehensionExpr in trigger | qunyanm | 2015-12-08 |
| * | Fix printing for ForallStmt. Previously we traverse the resolved forall | qunyanm | 2015-12-04 |
| * | Fix issue 113. Make sure the tempVar name used in ToString() method doesn't | qunyanm | 2015-12-03 |
| * | Fix issue 110. Set useImport to true when trying to registerTopLevelDecls | qunyanm | 2015-12-02 |
| * | Fix issue 111. Create a new BoundVar for each CasePattern of MatchCaseExpr when | qunyanm | 2015-11-30 |
| * | Made an adjustment in the printing of resolved forall expressions (previous c... | leino | 2015-11-28 |
| * | Merge | leino | 2015-11-27 |
| |\ |
|
| * | | Make cached results dependent on if a function is ghost or not | leino | 2015-11-27 |
| * | | autocontracts: Don't add modifies clause to ghost methods | leino | 2015-11-27 |
| | * | Fix issue 103. Emit the quantifiers for ForallStmt before AutoTrigger so that | qunyanm | 2015-11-25 |
| |/ |
|
| * | 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 |
| * | Fix issue 107. Instead of writing out StaticReceiverExpr as null valued | qunyanm | 2015-11-17 |
| * | Fix issue 100. Add an axiom for functionHandle to trigger off of the origial | qunyanm | 2015-11-17 |
| * | 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 |
| | * | 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 |
| * | Fixed location of blue dots to appear after semi-colons, not just before them. | leino | 2015-10-26 |
| * | 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 |
| * | 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 |
qunyanm
Richard L. Ford
Bryan Parno