From 407cfc5cd9bddb106e60d55684a78e660af87f88 Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Tue, 10 Jul 2012 16:08:44 -0700
Subject: Dafny: fixed ghost checking for labeled (i.e. named) expressions,
 changed to parallel syntax, other minor fixes

---
 Dafny/Compiler.cs | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'Dafny/Compiler.cs')

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
       }
-- 
cgit v1.2.3