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 | 407cfc5cd9bddb106e60d55684a78e660af87f88 (patch) | |
| tree | ad1ada34d480928783e997c85578f4f04ef82ae9 /Dafny/Compiler.cs | |
| parent | 8bc70b104efb559206a2b65e3f4151049dcb84ad (diff) | |
Dafny: fixed ghost checking for labeled (i.e. named) expressions, changed to parallel syntax, other minor fixes
Diffstat (limited to 'Dafny/Compiler.cs')
| -rw-r--r-- | Dafny/Compiler.cs | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs index 7f48e551..3864df8b 100644 --- a/Dafny/Compiler.cs +++ b/Dafny/Compiler.cs @@ -2184,6 +2184,8 @@ namespace Microsoft.Dafny { var e = (ConcreteSyntaxExpression)expr;
TrExpr(e.ResolvedExpression);
+ } else if (expr is NamedExpr) {
+ TrExpr(((NamedExpr)expr).Body);
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
}
|