1 files changed, 4 insertions, 4 deletions
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...
     {
       ...;