summaryrefslogtreecommitdiff
path: root/Source/Dafny/Rewriter.cs
Commit message (Expand)AuthorAge
* Removed Contract.Requires from method overrides (preconditions of overrides a...Gravatar Rustan Leino2016-01-06
* Fix issue 111. Create a new BoundVar for each CasePattern of MatchCaseExpr whenGravatar qunyanm2015-11-30
* MergeGravatar leino2015-11-27
|\
* | autocontracts: Don't add modifies clause to ghost methodsGravatar leino2015-11-27
| * Fix issue 103. Emit the quantifiers for ForallStmt before AutoTrigger so thatGravatar qunyanm2015-11-25
|/
* Introduced new datatype update syntax: D.(f := E)Gravatar leino2015-10-23
* Parsing and pretty printing of the new "existential guards" of the two kinds ...Gravatar leino2015-10-03
* Make quantifier splitting a two step processGravatar Clément Pit--Claudel2015-08-23
* Make `old` a special case for trigger generation.Gravatar Clément Pit--Claudel2015-08-21
* Factor out some AST visiting codeGravatar Clément Pit--Claudel2015-08-19
* Merge.Gravatar Clément Pit--Claudel2015-08-19
|\
* | Small cleanups, fixes, and refactoringsGravatar Clément Pit--Claudel2015-08-18
* | Start committing split quantifiersGravatar Clément Pit--Claudel2015-08-14
* | Start committing generated triggers when /autoTriggers is 1Gravatar Clément Pit--Claudel2015-08-14
* | Draft out a more advanced version of trigger generationGravatar Clément Pit--Claudel2015-08-19
* | Refactor the error reporting codeGravatar Clément Pit--Claudel2015-08-18
| * Change the induction heuristic for lemmas to also look in precondition for cl...Gravatar leino2015-08-12
| * Bug fixes and improvements in pretty printingGravatar leino2015-08-11
| * Removed the unused type ThisSurrogateGravatar leino2015-08-11
| * Moved discovery of induction variables into a Rewriter.Gravatar leino2015-08-11
|/
* fix for apparent typo in Rewriter.csGravatar Michael Lowell Roberts2015-07-20
* Merge my autoTriggers work into the master branchGravatar Clément Pit--Claudel2015-07-17
|\
* | Register the trigger generator as a a rewriter in the Resolver.Gravatar Clément Pit--Claudel2015-07-13
* | Make attributes enumerable.Gravatar Clément Pit--Claudel2015-07-13
| * Fix identifiers in nested match patterns not showing in the IDE bug. RememberGravatar qunyanm2015-06-29
|/
* Fix various bugs in nested match patterns listed in issue #83Gravatar qunyanm2015-06-19
* Added {:auto_generated} trigger, which indicates that a declaration was not e...Gravatar Rustan Leino2015-06-02
* Add an infinite set collection type.Gravatar qunyanm2015-05-29
* Allow MatchExpr and MatchStmt to have nested patterns. Such asGravatar qunyanm2015-05-14
* Fix issue #71. When substitute the forall's variables for those of theGravatar qunyanm2015-04-16
* Eliminate redundant checks of newtype and opaque function well-formedness fro...Gravatar chrishaw2015-04-02
* Fix issue #55 and #64. When performing type argument substitution for functionGravatar qunyanm2015-03-16
* This changeset changes the default visibility of a function/predicate body ou...Gravatar leino2015-03-09
* Fixed an encoding bug for newtypes (this fixes Issue #50)Gravatar Rustan Leino2015-01-27
* Switched use of List(IToken) in UserDefinedType to NameSegment/ExprDotName, s...Gravatar leino2015-01-23
* Fixed bug in opaque functions with type parametersGravatar leino2015-01-07
* Language change: All functions and methods declared lexically outside any cla...Gravatar leino2014-12-12
* Finished up refactoring of the new name segment parsing, AST, and resolution.Gravatar leino2014-12-07
* Snapshot, to be continuedGravatar leino2014-12-02
* Make autoreqs of free requires not freeGravatar Bryan Parno2014-10-27
* Allow autoReq in methods to generate auto-requirements on requiresGravatar Bryan Parno2014-10-27
* Don't process opaque functions more than once when generating auto-reqsGravatar Bryan Parno2014-10-27
* Fix fixup to opaque-function revealer to deal with zero-argument lemmasGravatar Bryan Parno2014-10-27
* Fix autoreq handling of quantifiersGravatar Bryan Parno2014-10-27
* Added an attribute :timeLimitMultiplier for setting relative time outs.Gravatar Bryan Parno2014-10-27
* Add an option to allow automatically generated requirements to be printedGravatar Bryan Parno2014-10-27
* Added types "char" and "string" (the latter being a synonym for "seq<char>").Gravatar leino2014-10-20
* MergeGravatar Dan Rosén2014-08-11
|\
* | Add higher-order-functions and some other goodiesGravatar Dan Rosén2014-08-11
| * Fixed bug Issue 37: expand type synonyms in more (hopefully all) places in th...Gravatar leino2014-08-02
|/
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 10:45:19 +0000