All ...Seq classes now gone

1 files changed, 12 insertions, 12 deletions

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 294abba3..1aaba87c 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -344,7 +344,7 @@ MapType<out Bpl.Type/*!*/ ty>
      IToken/*!*/ nnTok;

      List<Type>/*!*/ arguments = new List<Type>();

      Bpl.Type/*!*/ result;

-     TypeVariableSeq/*!*/ typeParameters = new TypeVariableSeq();

+     List<TypeVariable>/*!*/ typeParameters = new List<TypeVariable>();

    .)

   [ TypeParams<out nnTok, out typeParameters> (. tok = nnTok; .) ]

   "["                                         (.  if (tok == null) tok = t;  .)

@@ -356,13 +356,13 @@ MapType<out Bpl.Type/*!*/ ty>
   .)

   .

 

-TypeParams<out IToken/*!*/ tok, out Bpl.TypeVariableSeq/*!*/ typeParams>

+TypeParams<out IToken/*!*/ tok, out Bpl.List<TypeVariable>/*!*/ typeParams>

 = (.Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); List<IToken>/*!*/ typeParamToks; .)

   "<"    (.  tok = t;  .)

     Idents<out typeParamToks>

   ">"

   (.

-    typeParams = new TypeVariableSeq ();

+    typeParams = new List<TypeVariable> ();

     foreach(Token/*!*/ id in typeParamToks){

       Contract.Assert(id != null);

       typeParams.Add(new TypeVariable(id, id.val));}

@@ -443,7 +443,7 @@ Function<out List<Declaration>/*!*/ ds>
 = (. Contract.Ensures(Contract.ValueAtReturn(out ds) != null);

      ds = new List<Declaration>(); IToken/*!*/ z;

      IToken/*!*/ typeParamTok;

-     var typeParams = new TypeVariableSeq();

+     var typeParams = new List<TypeVariable>();

      var arguments = new List<Variable>();

      TypedIdent/*!*/ tyd;

      TypedIdent retTyd = null;

@@ -571,7 +571,7 @@ UserDefinedType<out Declaration/*!*/ decl, QKeyValue kv>
   ]

   (.

      if (synonym) {

-       TypeVariableSeq/*!*/ typeParams = new TypeVariableSeq();

+       List<TypeVariable>/*!*/ typeParams = new List<TypeVariable>();

        foreach(Token/*!*/ t in paramTokens){

          Contract.Assert(t != null);

          typeParams.Add(new TypeVariable(t, t.val));}

@@ -586,7 +586,7 @@ UserDefinedType<out Declaration/*!*/ decl, QKeyValue kv>
 /*------------------------------------------------------------------------*/

 Procedure<out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl>

 = (. Contract.Ensures(Contract.ValueAtReturn(out proc) != null); IToken/*!*/ x;

-     TypeVariableSeq/*!*/ typeParams;

+     List<TypeVariable>/*!*/ typeParams;

      List<Variable>/*!*/ ins, outs;

      List<Requires>/*!*/ pre = new List<Requires>();

      List<IdentifierExpr>/*!*/ mods = new List<IdentifierExpr>();

@@ -615,7 +615,7 @@ Procedure<out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl>
 

 Implementation<out Implementation/*!*/ impl>

 = (. Contract.Ensures(Contract.ValueAtReturn(out impl) != null); IToken/*!*/ x;

-     TypeVariableSeq/*!*/ typeParams;

+     List<TypeVariable>/*!*/ typeParams;

      List<Variable>/*!*/ ins, outs;

      List<Variable>/*!*/ locals;

      StmtList/*!*/ stmtList;

@@ -629,10 +629,10 @@ Implementation<out Implementation/*!*/ impl>
   .

 

 

-ProcSignature<bool allowWhereClausesOnFormals, out IToken/*!*/ name, out TypeVariableSeq/*!*/ typeParams,

+ProcSignature<bool allowWhereClausesOnFormals, out IToken/*!*/ name, out List<TypeVariable>/*!*/ typeParams,

               out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv>

 = (. Contract.Ensures(Contract.ValueAtReturn(out name) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); Contract.Ensures(Contract.ValueAtReturn(out ins) != null); Contract.Ensures(Contract.ValueAtReturn(out outs) != null);

-     IToken/*!*/ typeParamTok; typeParams = new TypeVariableSeq();

+     IToken/*!*/ typeParamTok; typeParams = new List<TypeVariable>();

      outs = new List<Variable>(); kv = null; .)

   { Attribute<ref kv> }

   Ident<out name>

@@ -1239,7 +1239,7 @@ ArrayExpression<out Expr/*!*/ e>
 AtomExpression<out Expr/*!*/ e>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd;

      List<Expr>/*!*/ es;  List<Variable>/*!*/ ds;  Trigger trig;

-     TypeVariableSeq/*!*/ typeParams;

+     List<TypeVariable>/*!*/ typeParams;

      IdentifierExpr/*!*/ id;

      QKeyValue kv;

      e = dummyExpr;

@@ -1412,10 +1412,10 @@ IfThenElseExpression<out Expr/*!*/ e>
   .

 

 

-QuantifierBody<IToken/*!*/ q, out TypeVariableSeq/*!*/ typeParams, out List<Variable>/*!*/ ds,

+QuantifierBody<IToken/*!*/ q, out List<TypeVariable>/*!*/ typeParams, out List<Variable>/*!*/ ds,

                out QKeyValue kv, out Trigger trig, out Expr/*!*/ body>

 = (. Contract.Requires(q != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); Contract.Ensures(Contract.ValueAtReturn(out ds) != null); Contract.Ensures(Contract.ValueAtReturn(out body) != null);

-     trig = null; typeParams = new TypeVariableSeq ();

+     trig = null; typeParams = new List<TypeVariable> ();

      IToken/*!*/ tok;

      kv = null;

      ds = new List<Variable> ();