From 8547ab2737f6bcb185398e4cbc3edde3847cb085 Mon Sep 17 00:00:00 2001
From: Ally Donaldson <unknown>
Date: Mon, 22 Jul 2013 10:35:39 +0100
Subject: Requires/EnsuresSeq replaced by List<Requires/Ensures>

---
 Source/Core/StandardVisitor.cs | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'Source/Core/StandardVisitor.cs')

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index ee873bd4..800a5494 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -248,10 +248,10 @@ namespace Microsoft.Boogie {
       @requires.Condition = this.VisitExpr(@requires.Condition);
       return @requires;
     }
-    public virtual RequiresSeq VisitRequiresSeq(RequiresSeq requiresSeq) {
+    public virtual List<Requires> VisitRequiresSeq(List<Requires> requiresSeq) {
       Contract.Requires(requiresSeq != null);
-      Contract.Ensures(Contract.Result<RequiresSeq>() != null);
-      for (int i = 0, n = requiresSeq.Length; i < n; i++)
+      Contract.Ensures(Contract.Result<List<Requires>>() != null);
+      for (int i = 0, n = requiresSeq.Count; i < n; i++)
         requiresSeq[i] = this.VisitRequires(requiresSeq[i]);
       return requiresSeq;
     }
@@ -261,10 +261,10 @@ namespace Microsoft.Boogie {
       @ensures.Condition = this.VisitExpr(@ensures.Condition);
       return @ensures;
     }
-    public virtual EnsuresSeq VisitEnsuresSeq(EnsuresSeq ensuresSeq) {
+    public virtual List<Ensures> VisitEnsuresSeq(List<Ensures> ensuresSeq) {
       Contract.Requires(ensuresSeq != null);
-      Contract.Ensures(Contract.Result<EnsuresSeq>() != null);
-      for (int i = 0, n = ensuresSeq.Length; i < n; i++)
+      Contract.Ensures(Contract.Result<List<Ensures>>() != null);
+      for (int i = 0, n = ensuresSeq.Count; i < n; i++)
         ensuresSeq[i] = this.VisitEnsures(ensuresSeq[i]);
       return ensuresSeq;
     }
-- 
cgit v1.2.3