summaryrefslogtreecommitdiff
path: root/Source/Dafny/Parser.cs
diff options
context:
space:
mode:
authorGravatar Jason Koenig <unknown>2012-07-30 17:22:28 -0700
committerGravatar Jason Koenig <unknown>2012-07-30 17:22:28 -0700
commitc3f4fae804fe07942cc1f0e4fc6e40b2542de645 (patch)
treeec5ddee8d2d2fa8c520cfe8c7bef199e187d0100 /Source/Dafny/Parser.cs
parente9534ceb03a09e5524709a6f9112d8c7fb1df711 (diff)
Dafny: support opening modules into the local scope
Diffstat (limited to 'Source/Dafny/Parser.cs')
-rw-r--r--Source/Dafny/Parser.cs6
1 files changed, 3 insertions, 3 deletions
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 244fe550..a7de690e 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -293,10 +293,10 @@ bool IsAttribute() {
Get();
QualifiedName(out idPath);
Expect(14);
- submodule = new AliasModuleDecl(idPath, id, parent);
+ submodule = new AliasModuleDecl(idPath, id, parent, opened);
} else if (la.kind == 14) {
Get();
- idPath = new List<IToken>(); idPath.Add(id); submodule = new AliasModuleDecl(idPath, id, parent);
+ idPath = new List<IToken>(); idPath.Add(id); submodule = new AliasModuleDecl(idPath, id, parent, opened);
} else if (la.kind == 15) {
Get();
QualifiedName(out idPath);
@@ -305,7 +305,7 @@ bool IsAttribute() {
QualifiedName(out idAssignment);
}
Expect(14);
- submodule = new AbstractModuleDecl(idPath, id, parent, idAssignment);
+ submodule = new AbstractModuleDecl(idPath, id, parent, idAssignment, opened);
} else SynErr(114);
} else SynErr(115);
}