diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-01-10 16:19:10 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-01-10 16:19:10 -0800 |
| commit | 3be3e9a226ee0defb514da6fe136ce7cadf9e17c (patch) | |
| tree | 40fefdd0b69ec16d46e54531be71aa33a7d3f5d2 /Dafny/Dafny.atg | |
| parent | 17d1562bae394856c24f09a2dac9f7404c5dd759 (diff) | |
Dafny: added test case for refinement and predicates (and fixed a parsing bug)
Diffstat (limited to 'Dafny/Dafny.atg')
| -rw-r--r-- | Dafny/Dafny.atg | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index 00dbe0a8..93c4d067 100644 --- a/Dafny/Dafny.atg +++ b/Dafny/Dafny.atg @@ -146,9 +146,9 @@ Dafny defaultModuleCreatedHere = true;
defaultModule = new DefaultModuleDecl();
}
- IToken idRefined = null;
+ IToken idRefined;
.)
- { "module" (. attrs = null; theImports = new List<string/*!*/>(); .)
+ { "module" (. attrs = null; idRefined = null; theImports = new List<string/*!*/>(); .)
{ Attribute<ref attrs> }
Ident<out id> (. defaultModule.ImportNames.Add(id.val); .)
[ "refines" Ident<out idRefined> ]
|