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/VCExpr/Boogie2VCExpr.cs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'Source/VCExpr/Boogie2VCExpr.cs')

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index cac6d95b..37bcda96 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -704,9 +704,9 @@ namespace Microsoft.Boogie.VCExprAST {
       Contract.Assert(false);
       throw new cce.UnreachableException();
     }
-    public override RequiresSeq VisitRequiresSeq(RequiresSeq requiresSeq) {
+    public override List<Requires> VisitRequiresSeq(List<Requires> requiresSeq) {
       //Contract.Requires(requiresSeq != null);
-      Contract.Ensures(Contract.Result<RequiresSeq>() != null);
+      Contract.Ensures(Contract.Result<List<Requires>>() != null);
       Contract.Assert(false);
       throw new cce.UnreachableException();
     }
@@ -716,9 +716,9 @@ namespace Microsoft.Boogie.VCExprAST {
       Contract.Assert(false);
       throw new cce.UnreachableException();
     }
-    public override EnsuresSeq VisitEnsuresSeq(EnsuresSeq ensuresSeq) {
+    public override List<Ensures> VisitEnsuresSeq(List<Ensures> ensuresSeq) {
       //Contract.Requires(ensuresSeq != null);
-      Contract.Ensures(Contract.Result<EnsuresSeq>() != null);
+      Contract.Ensures(Contract.Result<List<Ensures>>() != null);
       Contract.Assert(false);
       throw new cce.UnreachableException();
     }
-- 
cgit v1.2.3