From 7ee036cae0cc6a2d48786f18908f26de37136236 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Mon, 1 Apr 2013 14:28:37 -0700
Subject: Moved resolution of BinaryExpr.ResolveOp until the CheckTypeInference
 phase, where more type information is known Refactored
 ConcreteUpdateStatement to no longer inherit from ConcreteSyntaxStatement.
 Fixed numerous places where some recursive checks did not reach.

---
 Test/dafny2/StoreAndRetrieve.dfy | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'Test/dafny2')

diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy
index 93bf1812..1cc906f3 100644
--- a/Test/dafny2/StoreAndRetrieve.dfy
+++ b/Test/dafny2/StoreAndRetrieve.dfy
@@ -1,6 +1,6 @@
 abstract module A {
   import L = Library;
-  class {:autocontracts} StoreAndRetrieve<Thing> {
+  class {:autocontracts} StoreAndRetrieve<Thing(==)> {
     ghost var Contents: set<Thing>;
     predicate Valid
     {
@@ -26,7 +26,7 @@ abstract module A {
 }
 
 module B refines A {
-  class StoreAndRetrieve<Thing> {
+  class StoreAndRetrieve<Thing(==)> {
     var arr: seq<Thing>;
     predicate Valid
     {
@@ -52,14 +52,14 @@ module B refines A {
       }
       var k := arr[i];
       ...;
-      var a :| assume Contents == set x | x in a;
+      var a: seq<Thing> :| assume Contents == set x | x in a;
       arr := a;
     }
   }
 }
 
 module C refines B {
-  class StoreAndRetrieve<Thing> {
+  class StoreAndRetrieve<Thing(==)> {
     method Retrieve...
     {
       ...;
-- 
cgit v1.2.3