From 3e2bab90aac63622eff8fde33b1f5fcb97a5f6c5 Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Mon, 11 Jul 2011 17:22:32 -0700
Subject: Added s[..] syntax in anticipation of sequence forming operation.
 (also updated regression tests.)

---
 Source/Dafny/Dafny.atg | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'Source/Dafny/Dafny.atg')

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index f6e40722..bcd23618 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1354,7 +1354,9 @@ Suffix<ref Expression/*!*/ e>
                                                .)
           }
         )
-      | ".." Expression<out ee>                (. anyDots = true;  e1 = ee; .)
+      | ".."                                   (. anyDots = true; .)
+	    [ Expression<out ee>                   (. e1 = ee; .)
+	    ]
       )
       (. if (multipleIndices != null) {
            e = new MultiSelectExpr(x, e, multipleIndices);
@@ -1367,7 +1369,7 @@ Suffix<ref Expression/*!*/ e>
            }
            Contract.Assert(anyDots || e0 != null);
            if (anyDots) {
-             Contract.Assert(e0 != null || e1 != null);
+             //Contract.Assert(e0 != null || e1 != null);
              e = new SeqSelectExpr(x, false, e, e0, e1);
            } else if (e1 == null) {
              Contract.Assert(e0 != null);
-- 
cgit v1.2.3