diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-10-30 14:25:33 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-10-30 14:25:33 -0700 |
| commit | c3facb25dd5e290993a91a896a3b5606d0f4b795 (patch) | |
| tree | 1a11f6f2a46e8ae29ee99236b57fcdcc0640892e /Source/DafnyDriver/DafnyDriver.cs | |
| parent | d4472576ba4f4678f48313e69733254fb1e7017c (diff) | |
Removed the encoding that was used to distinguish datatype values by their type
parameters. Previously, this encoding was used in places like the antecedents
of function frame axioms. However, not all datatype constructors had this
information available, so it seems better (for now) to drop this information
altogether. When a full Boogie-term encoding of Dafny types is done, then it
would be appropriate revisit this issue.
Diffstat (limited to 'Source/DafnyDriver/DafnyDriver.cs')
0 files changed, 0 insertions, 0 deletions