index
:
debian-dafny
master
Debian packaging for Dafny
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Source
/
Dafny
/
Resolver.cs
Commit message (
Expand
)
Author
Age
*
Fix issue 131. Instead of crashing, report an error when an undefined member of
qunyanm
2016-02-09
*
Fix issue 125. Add the missing case 2 and 3 with refinement and opened imports.
qunyanm
2016-02-05
*
Fix issue 129. When looking for a constructor for which Dafny knows how to
qunyanm
2016-02-02
*
Implement module export so we can export a subset of items defined in the
qunyanm
2016-01-29
*
Implement 'extern' declaration modifier.
Richard L. Ford
2016-01-27
*
Mark temps that are generated in the resolver as auto-generated identifiers so
qunyanm
2016-01-20
*
Fix issue 118. When iteratively computing bounds, treat RefBoundedPool typed
qunyanm
2016-01-07
*
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
*
Fix issue 103. Emit the quantifiers for ForallStmt before AutoTrigger so that
qunyanm
2015-11-25
*
Fix issue 94. Allow tuple-based assignment in statement contexts.
qunyanm
2015-11-14
*
Fix issue 91 - Change how we compute the bounds of quantified variables so that
qunyanm
2015-10-29
*
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
*
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
*
Hover text includes #[_k-1] suffix for terms rewritten in prefix predicates/l...
Rustan Leino
2015-10-02
*
Removed some unused code.
Rustan Leino
2015-09-30
*
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
*
|
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
|
*
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
*
|
Refactored most of UnifyTypes calls into a ConstrainTypes method, preparing f...
leino
2015-08-31
|
/
*
Merge
Clément Pit--Claudel
2015-08-21
|
\
*
|
Cleanup a number of FIXMEs that I had left in the code
Clément Pit--Claudel
2015-08-20
|
*
Changed equality tests involving traits from using strings to using reference...
Rustan Leino
2015-08-20
|
/
*
Fixed bug in type unification
Rustan Leino
2015-08-20
*
Merge
Rustan Leino
2015-08-20
|
\
*
|
Refactored and improved bounds discovery
Rustan Leino
2015-08-19
|
*
Merge.
Clément Pit--Claudel
2015-08-19
|
|
\
|
|
/
|
/
|
|
*
Refactor calls to 'new CallCmd' and clear a few FIXMEs
Clément Pit--Claudel
2015-08-18
*
|
Update the way bounds are discovered to try to choose "better" bounds.
Bryan Parno
2015-08-17
|
*
Start committing split quantifiers
Clément Pit--Claudel
2015-08-14
|
*
Run the trigger rewriter after the quantifier splitter
Clément Pit--Claudel
2015-08-14
|
*
Refactor the error reporting code
Clément Pit--Claudel
2015-08-18
*
|
Bug fixes and improvements in pretty printing
leino
2015-08-11
*
|
Moved discovery of induction variables into a Rewriter.
leino
2015-08-11
|
/
*
Bug fix: check that assign-such-that constraint is of type boolean
Rustan Leino
2015-07-31
*
Fixed crash in resolution where, after reporting an error, the cases #type an...
Rustan Leino
2015-07-29
*
Clean up error reporting.
Clément Pit--Claudel
2015-07-27
*
Fix: Visual studio did not show warnings.
Clément Pit--Claudel
2015-07-23
*
clarified error message that occurs when the "opened" keyword is left off of ...
Michael Lowell Roberts
2015-07-20
[next]