Boogie:

* Added support for polymorphism in lambda expressions
* Little clean-up here and there
* Added 'then' keyword to emacs and latex modes

Dafny:
* Added support for fine-grained framing, using the back-tick syntax from Region Logic
* Internally, changed checking of reads clauses to use a local variable $_Frame, analogous to the $_Frame variable used in checking modifies clauses

1 files changed, 4 insertions, 4 deletions

diff --git a/Source/Core/AbsyExpr.ssc b/Source/Core/AbsyExpr.ssc
index ab834cb2..776ff8b3 100644
--- a/Source/Core/AbsyExpr.ssc
+++ b/Source/Core/AbsyExpr.ssc
@@ -565,7 +565,7 @@ namespace Microsoft.Boogie
   

   public class IdentifierExpr : Expr

   {

-    public string! Name;     // identifier symbol

+    public string! Name;    // identifier symbol

     public Variable Decl;   // identifier declaration

 

     /// <summary>

@@ -643,10 +643,10 @@ namespace Microsoft.Boogie
         return;

       }

       Decl = rc.LookUpVariable(Name);

-      if (rc.StateMode == ResolutionContext.State.StateLess && Decl is GlobalVariable) {

-        rc.Error(this, "cannot refer to a global variable in this context: {0}", Name);

-      } else if (Decl == null) {

+      if (Decl == null) {

         rc.Error(this, "undeclared identifier: {0}", Name);

+      } else if (rc.StateMode == ResolutionContext.State.StateLess && Decl is GlobalVariable) {

+        rc.Error(this, "cannot refer to a global variable in this context: {0}", Name);

       }

       if (Type != null) {

         Type = Type.ResolveType(rc);