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

(limited to 'Source/Core/BoogiePL.atg')

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 64ddbb50..9cd7d524 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -588,9 +588,9 @@ Procedure<out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl>
 = (. Contract.Ensures(Contract.ValueAtReturn(out proc) != null); IToken/*!*/ x;
      TypeVariableSeq/*!*/ typeParams;
      VariableSeq/*!*/ ins, outs;
-     RequiresSeq/*!*/ pre = new RequiresSeq();
+     List<Requires>/*!*/ pre = new List<Requires>();
      IdentifierExprSeq/*!*/ mods = new IdentifierExprSeq();
-     EnsuresSeq/*!*/ post = new EnsuresSeq();
+     List<Ensures>/*!*/ post = new List<Ensures>();
 
      VariableSeq/*!*/ locals = new VariableSeq();
      StmtList/*!*/ stmtList;
@@ -642,7 +642,7 @@ ProcSignature<bool allowWhereClausesOnFormals, out IToken/*!*/ name, out TypeVar
   .
 
 
-Spec<RequiresSeq/*!*/ pre, IdentifierExprSeq/*!*/ mods, EnsuresSeq/*!*/ post>
+Spec<List<Requires>/*!*/ pre, IdentifierExprSeq/*!*/ mods, List<Ensures>/*!*/ post>
 = (.Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); TokenSeq/*!*/ ms; .)
   ( "modifies"
     [ Idents<out ms>        (. foreach(IToken/*!*/ m in ms){
@@ -656,7 +656,7 @@ Spec<RequiresSeq/*!*/ pre, IdentifierExprSeq/*!*/ mods, EnsuresSeq/*!*/ post>
   )
   .
 
-SpecPrePost<bool free, RequiresSeq/*!*/ pre, EnsuresSeq/*!*/ post>
+SpecPrePost<bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post>
 = (. Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null; .)
   ( "requires"              (. tok = t; .)
     { Attribute<ref kv> }
-- 
cgit v1.2.3