From 4cbe4583b329a39dee2b4b456758cafbe7e2fa79 Mon Sep 17 00:00:00 2001
From: Dan Rosén <danr@chalmers.se>
Date: Mon, 11 Aug 2014 14:57:27 -0700
Subject: Add higher-order-functions and some other goodies

  * The reads clause now needs to be self framing.

  * The requires clause now needs to be framed by the reads clause.

  * There are one-shot lambdas, with a single arrow, but they will probably be
    removed.

  * There is a {:heapQuantifier} attribute to quantifiers, but they will
    probably be removed.

  * Add smart handling of type variables

  * Add < and > for datatype & type parameter
---
 Source/DafnyExtension/IdentifierTagger.cs | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'Source/DafnyExtension/IdentifierTagger.cs')

diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index 4cf752fb..beab8303 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -243,9 +243,12 @@ namespace DafnyLanguage
       } else if (expr is IdentifierExpr) {
         var e = (IdentifierExpr)expr;
         IdRegion.Add(regions, e.tok, e.Var, false, module);
-      } else if (expr is FieldSelectExpr) {
-        var e = (FieldSelectExpr)expr;
-        IdRegion.Add(regions, e.tok, e.Field, e.Type, "field", false, module);
+      } else if (expr is MemberSelectExpr) {
+        var e = (MemberSelectExpr)expr;
+        var field = e.Member as Field;
+        if (field != null) {
+          IdRegion.Add(regions, e.tok, field, e.Type, "field", false, module);
+        }
       } else if (expr is LetExpr) {
         var e = (LetExpr)expr;
         foreach (var bv in e.BoundVars) {
-- 
cgit v1.2.3