diff options
| author |  Jason Koenig <unknown> | 2012-07-10 16:08:44 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2012-07-10 16:08:44 -0700 |
| commit | e2fa35ca7a769e483014ec03a7c91faf2196f678 (patch) | |
| tree | c87bd120340c44d55119ef603cb83dcbf6a6aeb7 /Source/Dafny/Resolver.cs | |
| parent | 326e42ddf27bec7b8eff9909143a012a250a787d (diff) | |
Dafny: fixed ghost checking for labeled (i.e. named) expressions, changed to parallel syntax, other minor fixes
Diffstat (limited to 'Source/Dafny/Resolver.cs')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 71210c9f..16804d8c 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -4421,8 +4421,9 @@ namespace Microsoft.Dafny { return;
}
} else if (expr is NamedExpr) {
- if (moduleInfo.IsGhost) return;
- else CheckIsNonGhost(((NamedExpr)expr).Body);
+ if (!moduleInfo.IsGhost)
+ CheckIsNonGhost(((NamedExpr)expr).Body);
+ return;
}
foreach (var ee in expr.SubExpressions) {
|