diff options
| author |  Rustan Leino <unknown> | 2013-12-30 17:12:28 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-12-30 17:12:28 -0800 |
| commit | 73ced41e0a39cf3133e6f34328d24a39aeb2e60e (patch) | |
| tree | 2be35c31a5c3d97b2f4c4b700e9827944619f6c9 /Source/Dafny/Dafny.atg | |
| parent | 24603296188f3ebd166a0a89da0edac0ebf76d89 (diff) | |
| parent | db17d7c604d9deb30147cdd0787b2ad342e0f021 (diff) | |
Merge
Diffstat (limited to 'Source/Dafny/Dafny.atg')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 5254d439..c7bae4b5 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -487,10 +487,9 @@ IteratorDecl<ModuleDefinition module, out IteratorDecl/*!*/ iter> bool signatureOmitted = false;
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- IToken iteratorKeywordTok;
.)
SYNC
- "iterator" (. iteratorKeywordTok = t; .)
+ "iterator"
{ Attribute<ref attrs> }
NoUSIdent<out id>
(
@@ -506,7 +505,7 @@ IteratorDecl<ModuleDefinition module, out IteratorDecl/*!*/ iter> { IteratorSpec<reads, mod, decreases, req, ens, yieldReq, yieldEns, ref readsAttrs, ref modAttrs, ref decrAttrs> }
[ BlockStmt<out body, out bodyStart, out bodyEnd>
]
- (. iter = new IteratorDecl(iteratorKeywordTok, id, id.val, module, typeArgs, ins, outs,
+ (. iter = new IteratorDecl(id, id.val, module, typeArgs, ins, outs,
new Specification<FrameExpression>(reads, readsAttrs),
new Specification<FrameExpression>(mod, modAttrs),
new Specification<Expression>(decreases, decrAttrs),
|