All ...Seq classes now gone

10 files changed, 221 insertions, 232 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 29f826f7..0436f846 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -192,7 +192,7 @@ namespace Microsoft.Boogie {
     public void Emit(TokenTextWriter stream) {

       Contract.Requires(stream != null);

       stream.SetToken(this);

-      Emitter.Declarations(this.TopLevelDeclarations, stream);

+      this.TopLevelDeclarations.Emit(stream);

     }

 

     public void ProcessDatatypeConstructors() {

@@ -689,7 +689,7 @@ namespace Microsoft.Boogie {
         blocks.Add(exit);

         Implementation loopImpl =

             new Implementation(Token.NoToken, loopProc.Name,

-                                new TypeVariableSeq(), inputs, outputs, new List<Variable>(), blocks);

+                                new List<TypeVariable>(), inputs, outputs, new List<Variable>(), blocks);

         loopImpl.Proc = loopProc;

         loopImpls.Add(loopImpl);

 

@@ -1257,7 +1257,7 @@ namespace Microsoft.Boogie {
   }

 

   public class TypeSynonymDecl : NamedDeclaration {

-    public TypeVariableSeq/*!*/ TypeParameters;

+    public List<TypeVariable>/*!*/ TypeParameters;

     public Type/*!*/ Body;

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -1267,7 +1267,7 @@ namespace Microsoft.Boogie {
 

 

     public TypeSynonymDecl(IToken/*!*/ tok, string/*!*/ name,

-                           TypeVariableSeq/*!*/ typeParams, Type/*!*/ body)

+                           List<TypeVariable>/*!*/ typeParams, Type/*!*/ body)

       : base(tok, name) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

@@ -1277,7 +1277,7 @@ namespace Microsoft.Boogie {
       this.Body = body;

     }

     public TypeSynonymDecl(IToken/*!*/ tok, string/*!*/ name,

-                           TypeVariableSeq/*!*/ typeParams, Type/*!*/ body, QKeyValue kv)

+                           List<TypeVariable>/*!*/ typeParams, Type/*!*/ body, QKeyValue kv)

       : base(tok, name) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

@@ -1796,7 +1796,7 @@ namespace Microsoft.Boogie {
   }

 

   public abstract class DeclWithFormals : NamedDeclaration {

-    public TypeVariableSeq/*!*/ TypeParameters;

+    public List<TypeVariable>/*!*/ TypeParameters;

     public /*readonly--except in StandardVisitor*/ List<Variable>/*!*/ InParams, OutParams;

 

     [ContractInvariantMethod]

@@ -1806,7 +1806,7 @@ namespace Microsoft.Boogie {
       Contract.Invariant(OutParams != null);

     }

 

-    public DeclWithFormals(IToken tok, string name, TypeVariableSeq typeParams,

+    public DeclWithFormals(IToken tok, string name, List<TypeVariable> typeParams,

                             List<Variable> inParams, List<Variable> outParams)

       : base(tok, name) {

       Contract.Requires(inParams != null);

@@ -1995,14 +1995,14 @@ namespace Microsoft.Boogie {
     private bool neverTriggerComputed;

 

     public Function(IToken tok, string name, List<Variable> args, Variable result)

-      : this(tok, name, new TypeVariableSeq(), args, result, null) {

+      : this(tok, name, new List<TypeVariable>(), args, result, null) {

       Contract.Requires(result != null);

       Contract.Requires(args != null);

       Contract.Requires(name != null);

       Contract.Requires(tok != null);

-      //:this(tok, name, new TypeVariableSeq(), args, result, null);

+      //:this(tok, name, new List<TypeVariable>(), args, result, null);

     }

-    public Function(IToken tok, string name, TypeVariableSeq typeParams, List<Variable> args, Variable result)

+    public Function(IToken tok, string name, List<TypeVariable> typeParams, List<Variable> args, Variable result)

       : this(tok, name, typeParams, args, result, null) {

       Contract.Requires(result != null);

       Contract.Requires(args != null);

@@ -2012,14 +2012,14 @@ namespace Microsoft.Boogie {
       //:this(tok, name, typeParams, args, result, null);

     }

     public Function(IToken tok, string name, List<Variable> args, Variable result, string comment)

-      : this(tok, name, new TypeVariableSeq(), args, result, comment) {

+      : this(tok, name, new List<TypeVariable>(), args, result, comment) {

       Contract.Requires(result != null);

       Contract.Requires(args != null);

       Contract.Requires(name != null);

       Contract.Requires(tok != null);

-      //:this(tok, name, new TypeVariableSeq(), args, result, comment);

+      //:this(tok, name, new List<TypeVariable>(), args, result, comment);

     }

-    public Function(IToken tok, string name, TypeVariableSeq typeParams, List<Variable> args, Variable/*!*/ result, string comment)

+    public Function(IToken tok, string name, List<TypeVariable> typeParams, List<Variable> args, Variable/*!*/ result, string comment)

       : base(tok, name, typeParams, args, new List<Variable> { result }) {

       Contract.Requires(result != null);

       Contract.Requires(args != null);

@@ -2028,7 +2028,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(tok != null);

       Comment = comment;

     }

-    public Function(IToken tok, string name, TypeVariableSeq typeParams, List<Variable> args, Variable result,

+    public Function(IToken tok, string name, List<TypeVariable> typeParams, List<Variable> args, Variable result,

                     string comment, QKeyValue kv)

       : this(tok, name, typeParams, args, result, comment) {

       Contract.Requires(args != null);

@@ -2143,7 +2143,7 @@ namespace Microsoft.Boogie {
         callArgs.Add(new IdentifierExpr(f.tok, nm));

         i++;

       }

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

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

       foreach (TypeVariable/*!*/ t in TypeParameters) {

         Contract.Assert(t != null);

         quantifiedTypeVars.Add(new TypeVariable(Token.NoToken, t.Name));

@@ -2378,7 +2378,7 @@ namespace Microsoft.Boogie {
     [Rep]

     public readonly ProcedureSummary/*!*/ Summary;

 

-    public Procedure(IToken/*!*/ tok, string/*!*/ name, TypeVariableSeq/*!*/ typeParams, List<Variable>/*!*/ inParams, List<Variable>/*!*/ outParams,

+    public Procedure(IToken/*!*/ tok, string/*!*/ name, List<TypeVariable>/*!*/ typeParams, List<Variable>/*!*/ inParams, List<Variable>/*!*/ outParams,

       List<Requires>/*!*/ requires, List<IdentifierExpr>/*!*/ modifies, List<Ensures>/*!*/ ensures)

       : this(tok, name, typeParams, inParams, outParams, requires, modifies, ensures, null) {

       Contract.Requires(tok != null);

@@ -2392,7 +2392,7 @@ namespace Microsoft.Boogie {
       //:this(tok, name, typeParams, inParams, outParams, requires, modifies, ensures, null);

     }

 

-    public Procedure(IToken/*!*/ tok, string/*!*/ name, TypeVariableSeq/*!*/ typeParams, List<Variable>/*!*/ inParams, List<Variable>/*!*/ outParams,

+    public Procedure(IToken/*!*/ tok, string/*!*/ name, List<TypeVariable>/*!*/ typeParams, List<Variable>/*!*/ inParams, List<Variable>/*!*/ outParams,

       List<Requires>/*!*/ @requires, List<IdentifierExpr>/*!*/ @modifies, List<Ensures>/*!*/ @ensures, QKeyValue kv

       )

       : base(tok, name, typeParams, inParams, outParams) {

@@ -2534,7 +2534,7 @@ namespace Microsoft.Boogie {
       public LoopProcedure(Implementation impl, Block header,

                            List<Variable> inputs, List<Variable> outputs, List<IdentifierExpr> globalMods)

           : base(Token.NoToken, impl.Name + "_loop_" + header.ToString(),

-               new TypeVariableSeq(), inputs, outputs,

+               new List<TypeVariable>(), inputs, outputs,

                new List<Requires>(), globalMods, new List<Ensures>())

       {

           enclosingImpl = impl;

@@ -2641,7 +2641,7 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public Implementation(IToken tok, string name, TypeVariableSeq typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> localVariables, [Captured] StmtList structuredStmts, QKeyValue kv)

+    public Implementation(IToken tok, string name, List<TypeVariable> typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> localVariables, [Captured] StmtList structuredStmts, QKeyValue kv)

       : this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, kv, new Errors()) {

       Contract.Requires(structuredStmts != null);

       Contract.Requires(localVariables != null);

@@ -2653,7 +2653,7 @@ namespace Microsoft.Boogie {
       //:this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, new Errors());

     }

 

-    public Implementation(IToken tok, string name, TypeVariableSeq typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> localVariables, [Captured] StmtList structuredStmts)

+    public Implementation(IToken tok, string name, List<TypeVariable> typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> localVariables, [Captured] StmtList structuredStmts)

       : this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, new Errors()) {

       Contract.Requires(structuredStmts != null);

       Contract.Requires(localVariables != null);

@@ -2665,7 +2665,7 @@ namespace Microsoft.Boogie {
       //:this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, new Errors());

     }

 

-    public Implementation(IToken tok, string name, TypeVariableSeq typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> localVariables, [Captured] StmtList structuredStmts, Errors errorHandler)

+    public Implementation(IToken tok, string name, List<TypeVariable> typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> localVariables, [Captured] StmtList structuredStmts, Errors errorHandler)

       : this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, errorHandler) {

       Contract.Requires(errorHandler != null);

       Contract.Requires(structuredStmts != null);

@@ -2680,7 +2680,7 @@ namespace Microsoft.Boogie {
 

     public Implementation(IToken/*!*/ tok,

       string/*!*/ name,

-      TypeVariableSeq/*!*/ typeParams,

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

       List<Variable>/*!*/ inParams,

       List<Variable>/*!*/ outParams,

       List<Variable>/*!*/ localVariables,

@@ -2705,7 +2705,7 @@ namespace Microsoft.Boogie {
       Attributes = kv;

     }

 

-    public Implementation(IToken tok, string name, TypeVariableSeq typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> localVariables, [Captured] List<Block/*!*/> block)

+    public Implementation(IToken tok, string name, List<TypeVariable> typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> localVariables, [Captured] List<Block/*!*/> block)

       : this(tok, name, typeParams, inParams, outParams, localVariables, block, null) {

       Contract.Requires(cce.NonNullElements(block));

       Contract.Requires(localVariables != null);

@@ -2719,7 +2719,7 @@ namespace Microsoft.Boogie {
 

     public Implementation(IToken/*!*/ tok,

       string/*!*/ name,

-      TypeVariableSeq/*!*/ typeParams,

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

       List<Variable>/*!*/ inParams,

       List<Variable>/*!*/ outParams,

       List<Variable>/*!*/ localVariables,

@@ -3209,33 +3209,22 @@ namespace Microsoft.Boogie {
     }

   }

 

-  #region Generic Sequences

-  //---------------------------------------------------------------------

-  // Generic Sequences

-  //---------------------------------------------------------------------

+  #region Helper methods for generic Sequences

 

-  public sealed class TypeVariableSeq : List<TypeVariable> {

-    public TypeVariableSeq(params TypeVariable[]/*!*/ args)

-      : base(args) {

-      Contract.Requires(args != null);

-    }

-    public TypeVariableSeq(TypeVariableSeq/*!*/ varSeq)

-      : base(varSeq) {

-      Contract.Requires(varSeq != null);

-    }

-    public void AppendWithoutDups(TypeVariableSeq s1) {

+  public static class TypeVariableSeqAlgorithms {

+    public static void AppendWithoutDups(this List<TypeVariable> tvs, List<TypeVariable> s1) {

       Contract.Requires(s1 != null);

       for (int i = 0; i < s1.Count; i++) {

         TypeVariable/*!*/ next = s1[i];

         Contract.Assert(next != null);

-        if (!this.Contains(next))

-          this.Add(next);

+        if (!tvs.Contains(next))

+          tvs.Add(next);

       }

     }

   }

 

   public static class Emitter {

-    public static void Declarations(List<Declaration/*!*/>/*!*/ decls, TokenTextWriter stream) {

+    public static void Emit(this List<Declaration/*!*/>/*!*/ decls, TokenTextWriter stream) {

       Contract.Requires(stream != null);

       Contract.Requires(cce.NonNullElements(decls));

       bool first = true;

@@ -3313,7 +3302,7 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public static void Emit(this TypeVariableSeq tvs, TokenTextWriter stream, string separator) {

+    public static void Emit(this List<TypeVariable> tvs, TokenTextWriter stream, string separator) {

       Contract.Requires(separator != null);

       Contract.Requires(stream != null);

       string sep = "";

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index dcc6d6e2..70ce610d 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1494,7 +1494,7 @@ namespace Microsoft.Boogie {
             // quick path

             return Type.Bool;

           }

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

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

           unifiable.AddRange(arg0type.FreeVariables);

           unifiable.AddRange(arg1type.FreeVariables);

 

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index fe0748a9..067edc00 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -46,7 +46,7 @@ namespace Microsoft.Boogie {
   }

   [ContractClass(typeof(BinderExprContracts))]

   public abstract class BinderExpr : Expr {

-    public TypeVariableSeq/*!*/ TypeParameters;

+    public List<TypeVariable>/*!*/ TypeParameters;

     public List<Variable>/*!*/ Dummies;

     public QKeyValue Attributes;

     public Expr/*!*/ Body;

@@ -58,7 +58,7 @@ namespace Microsoft.Boogie {
     }

 

 

-    public BinderExpr(IToken/*!*/ tok, TypeVariableSeq/*!*/ typeParameters,

+    public BinderExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParameters,

                       List<Variable>/*!*/ dummies, QKeyValue kv, Expr/*!*/ body)

       : base(tok)

       {

@@ -191,11 +191,11 @@ namespace Microsoft.Boogie {
       }

     }

 

-    protected TypeVariableSeq GetUnmentionedTypeParameters() {

-      Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);

-      TypeVariableSeq/*!*/ dummyParameters = Type.FreeVariablesIn(new List<Type>(Dummies.Select(Item => Item.TypedIdent.Type).ToArray()));

+    protected List<TypeVariable> GetUnmentionedTypeParameters() {

+      Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);

+      List<TypeVariable>/*!*/ dummyParameters = Type.FreeVariablesIn(new List<Type>(Dummies.Select(Item => Item.TypedIdent.Type).ToArray()));

       Contract.Assert(dummyParameters != null);

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

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

       foreach (TypeVariable/*!*/ var in TypeParameters) {

         Contract.Assert(var != null);

         if (!dummyParameters.Contains(var))

@@ -421,7 +421,7 @@ namespace Microsoft.Boogie {
   }

 

   public class ForallExpr : QuantifierExpr {

-    public ForallExpr(IToken/*!*/ tok, TypeVariableSeq/*!*/ typeParams,

+    public ForallExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParams,

                       List<Variable>/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body)

       : base(tok, typeParams, dummies, kv, triggers, body) {

       Contract.Requires(tok != null);

@@ -431,20 +431,20 @@ namespace Microsoft.Boogie {
       Contract.Requires(dummies.Count + typeParams.Count > 0);

     }

     public ForallExpr(IToken tok, List<Variable> dummies, Trigger triggers, Expr body)

-      : base(tok, new TypeVariableSeq(), dummies, null, triggers, body) {

+      : base(tok, new List<TypeVariable>(), dummies, null, triggers, body) {

       Contract.Requires(body != null);

       Contract.Requires(dummies != null);

       Contract.Requires(tok != null);

       Contract.Requires(dummies.Count > 0);

     }

     public ForallExpr(IToken tok, List<Variable> dummies, Expr body)

-      : base(tok, new TypeVariableSeq(), dummies, null, null, body) {

+      : base(tok, new List<TypeVariable>(), dummies, null, null, body) {

       Contract.Requires(body != null);

       Contract.Requires(dummies != null);

       Contract.Requires(tok != null);

       Contract.Requires(dummies.Count > 0);

     }

-    public ForallExpr(IToken tok, TypeVariableSeq typeParams, List<Variable> dummies, Expr body)

+    public ForallExpr(IToken tok, List<TypeVariable> typeParams, List<Variable> dummies, Expr body)

       : base(tok, typeParams, dummies, null, null, body) {

       Contract.Requires(body != null);

       Contract.Requires(dummies != null);

@@ -467,7 +467,7 @@ namespace Microsoft.Boogie {
   }

 

   public class ExistsExpr : QuantifierExpr {

-    public ExistsExpr(IToken/*!*/ tok, TypeVariableSeq/*!*/ typeParams, List<Variable>/*!*/ dummies,

+    public ExistsExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParams, List<Variable>/*!*/ dummies,

                       QKeyValue kv, Trigger triggers, Expr/*!*/ body)

       : base(tok, typeParams, dummies, kv, triggers, body) {

       Contract.Requires(tok != null);

@@ -477,14 +477,14 @@ namespace Microsoft.Boogie {
       Contract.Requires(dummies.Count + typeParams.Count > 0);

     }

     public ExistsExpr(IToken tok, List<Variable> dummies, Trigger triggers, Expr body)

-      : base(tok, new TypeVariableSeq(), dummies, null, triggers, body) {

+      : base(tok, new List<TypeVariable>(), dummies, null, triggers, body) {

       Contract.Requires(body != null);

       Contract.Requires(dummies != null);

       Contract.Requires(tok != null);

       Contract.Requires(dummies.Count > 0);

     }

     public ExistsExpr(IToken tok, List<Variable> dummies, Expr body)

-      : base(tok, new TypeVariableSeq(), dummies, null, null, body) {

+      : base(tok, new List<TypeVariable>(), dummies, null, null, body) {

       Contract.Requires(body != null);

       Contract.Requires(dummies != null);

       Contract.Requires(tok != null);

@@ -515,7 +515,7 @@ namespace Microsoft.Boogie {
 

     public readonly int SkolemId;

 

-    public QuantifierExpr(IToken/*!*/ tok, TypeVariableSeq/*!*/ typeParameters,

+    public QuantifierExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParameters,

                           List<Variable>/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body)

       : base(tok, typeParameters, dummies, kv, body) {

       Contract.Requires(tok != null);

@@ -661,7 +661,7 @@ namespace Microsoft.Boogie {
       // Check that type parameters occur in the types of the

       // dummies, or otherwise in the triggers. This can only be

       // done after typechecking

-      TypeVariableSeq/*!*/ unmentionedParameters = GetUnmentionedTypeParameters();

+      List<TypeVariable>/*!*/ unmentionedParameters = GetUnmentionedTypeParameters();

       Contract.Assert(unmentionedParameters != null);

 

       if (unmentionedParameters.Count > 0) {

@@ -696,7 +696,7 @@ namespace Microsoft.Boogie {
 

 

   public class LambdaExpr : BinderExpr {

-    public LambdaExpr(IToken/*!*/ tok, TypeVariableSeq/*!*/ typeParameters,

+    public LambdaExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParameters,

                       List<Variable>/*!*/ dummies, QKeyValue kv, Expr/*!*/ body)

       : base(tok, typeParameters, dummies, kv, body) {

       Contract.Requires(tok != null);

@@ -735,7 +735,7 @@ namespace Microsoft.Boogie {
       // Check that type parameters occur in the types of the

       // dummies, or otherwise in the triggers. This can only be

       // done after typechecking

-      TypeVariableSeq/*!*/ unmentionedParameters = GetUnmentionedTypeParameters();

+      List<TypeVariable>/*!*/ unmentionedParameters = GetUnmentionedTypeParameters();

       Contract.Assert(unmentionedParameters != null);

 

       if (unmentionedParameters.Count > 0) {

diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index 64c4b699..75cb7f4a 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -74,14 +74,14 @@ namespace Microsoft.Boogie {
         return true;

       Type thatType = that as Type;

       return thatType != null && this.Equals(thatType,

-                                             new TypeVariableSeq(),

-                                             new TypeVariableSeq());

+                                             new List<TypeVariable>(),

+                                             new List<TypeVariable>());

     }

 

     [Pure]

     public abstract bool Equals(Type/*!*/ that,

-                                TypeVariableSeq/*!*/ thisBoundVariables,

-                                TypeVariableSeq/*!*/ thatBoundVariables);

+                                List<TypeVariable>/*!*/ thisBoundVariables,

+                                List<TypeVariable>/*!*/ thatBoundVariables);

 

     // used to skip leading type annotations (subexpressions of the

     // resulting type might still contain annotations)

@@ -102,11 +102,11 @@ namespace Microsoft.Boogie {
     /// </summary>

     public bool Unify(Type that) {

       Contract.Requires(that != null);

-      return Unify(that, new TypeVariableSeq(), new Dictionary<TypeVariable/*!*/, Type/*!*/>());

+      return Unify(that, new List<TypeVariable>(), new Dictionary<TypeVariable/*!*/, Type/*!*/>());

     }

 

     public abstract bool Unify(Type/*!*/ that,

-                               TypeVariableSeq/*!*/ unifiableVariables,

+                               List<TypeVariable>/*!*/ unifiableVariables,

       // an idempotent substitution that describes the

       // unification result up to a certain point

                                IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier);

@@ -125,11 +125,11 @@ namespace Microsoft.Boogie {
     // no such unifier exists. The unifier is not allowed to subtitute any

     // type variables other than the ones in "unifiableVariables"

     public IDictionary<TypeVariable!, Type!> Unify(Type! that,

-                                                   TypeVariableSeq! unifiableVariables) {

+                                                   List<TypeVariable>! unifiableVariables) {

       Dictionary<TypeVariable!, Type!>! result = new Dictionary<TypeVariable!, Type!> ();

       try {

         this.Unify(that, unifiableVariables,

-                   new TypeVariableSeq (), new TypeVariableSeq (), result);

+                   new List<TypeVariable> (), new List<TypeVariable> (), result);

       } catch (UnificationFailedException) {

         return null;

       }

@@ -139,7 +139,7 @@ namespace Microsoft.Boogie {
     // Compute an idempotent most general unifier and add the result to the argument

     // unifier. The result is true iff the unification succeeded

     public bool Unify(Type! that,

-                      TypeVariableSeq! unifiableVariables,

+                      List<TypeVariable>! unifiableVariables,

                       // given mappings that need to be taken into account

                       // the old unifier has to be idempotent as well

                       IDictionary<TypeVariable!, Type!>! unifier)

@@ -148,7 +148,7 @@ namespace Microsoft.Boogie {
  Contract.Requires(IsIdempotent(unifier));

       try {

         this.Unify(that, unifiableVariables,

-                   new TypeVariableSeq (), new TypeVariableSeq (), unifier);

+                   new List<TypeVariable> (), new List<TypeVariable> (), unifier);

       } catch (UnificationFailedException) {

         return false;

       }

@@ -156,9 +156,9 @@ namespace Microsoft.Boogie {
     }

 

     public abstract void Unify(Type! that,

-                               TypeVariableSeq! unifiableVariables,

-                               TypeVariableSeq! thisBoundVariables,

-                               TypeVariableSeq! thatBoundVariables,

+                               List<TypeVariable>! unifiableVariables,

+                               List<TypeVariable>! thisBoundVariables,

+                               List<TypeVariable>! thatBoundVariables,

                                // an idempotent substitution that describes the

                                // unification result up to a certain point

                                IDictionary<TypeVariable!, Type!>! result);

@@ -179,11 +179,11 @@ namespace Microsoft.Boogie {
 

     [Pure]

     public override int GetHashCode() {

-      return this.GetHashCode(new TypeVariableSeq());

+      return this.GetHashCode(new List<TypeVariable>());

     }

 

     [Pure]

-    public abstract int GetHashCode(TypeVariableSeq/*!*/ boundVariables);

+    public abstract int GetHashCode(List<TypeVariable>/*!*/ boundVariables);

 

     //-----------  Resolution  ----------------------------------

 

@@ -201,7 +201,7 @@ namespace Microsoft.Boogie {
     }

 

     // determine the free variables in a type, in the order in which the variables occur

-    public abstract TypeVariableSeq/*!*/ FreeVariables {

+    public abstract List<TypeVariable>/*!*/ FreeVariables {

       get;

     }

 

@@ -364,7 +364,7 @@ namespace Microsoft.Boogie {
 

 #if OLD_UNIFICATION

     public static IDictionary<TypeVariable!, Type!>!

-                  MatchArgumentTypes(TypeVariableSeq! typeParams,

+                  MatchArgumentTypes(List<TypeVariable>! typeParams,

                                      List<Type>! formalArgs,

                                      List<Expr>! actualArgs,

                                      List<Type> formalOuts,

@@ -375,8 +375,8 @@ namespace Microsoft.Boogie {
  Contract.Requires(formalArgs.Length == actualArgs.Length);

  Contract.Requires(formalOuts == null <==> actualOuts == null);

  Contract.Requires(formalOuts != null ==> formalOuts.Length == actualOuts.Length);

-      TypeVariableSeq! boundVarSeq0 = new TypeVariableSeq ();

-      TypeVariableSeq! boundVarSeq1 = new TypeVariableSeq ();

+      List<TypeVariable>! boundVarSeq0 = new List<TypeVariable> ();

+      List<TypeVariable>! boundVarSeq1 = new List<TypeVariable> ();

       Dictionary<TypeVariable!, Type!>! subst = new Dictionary<TypeVariable!, Type!>();

 

       for (int i = 0; i < formalArgs.Length; ++i) {

@@ -436,7 +436,7 @@ namespace Microsoft.Boogie {
     }

 #else

     public static IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/

-                  MatchArgumentTypes(TypeVariableSeq/*!*/ typeParams,

+                  MatchArgumentTypes(List<TypeVariable>/*!*/ typeParams,

                                      List<Type>/*!*/ formalArgs,

                                      List<Expr>/*!*/ actualArgs,

                                      List<Type> formalOuts,

@@ -505,7 +505,7 @@ namespace Microsoft.Boogie {
     //------------  on concrete types, substitute the result into the

     //------------  result type. Null is returned for type errors

 

-    public static List<Type> CheckArgumentTypes(TypeVariableSeq/*!*/ typeParams,

+    public static List<Type> CheckArgumentTypes(List<TypeVariable>/*!*/ typeParams,

                                              out List<Type/*!*/>/*!*/ actualTypeParams,

                                              List<Type>/*!*/ formalIns,

                                              List<Expr>/*!*/ actualIns,

@@ -555,7 +555,7 @@ namespace Microsoft.Boogie {
         Contract.Assert(t != null);

         actualResults.Add(t.Substitute(subst));

       }

-      TypeVariableSeq resultFreeVars = FreeVariablesIn(actualResults);

+      List<TypeVariable> resultFreeVars = FreeVariablesIn(actualResults);

       if (previousErrorCount != tc.ErrorCount) {

         // errors occured when matching the formal arguments

         // in case we have been able to substitute all type parameters,

@@ -577,7 +577,7 @@ namespace Microsoft.Boogie {
 

     // about the same as Type.CheckArgumentTypes, but without

     // detailed error reports

-    public static Type/*!*/ InferValueType(TypeVariableSeq/*!*/ typeParams,

+    public static Type/*!*/ InferValueType(List<TypeVariable>/*!*/ typeParams,

                                        List<Type>/*!*/ formalArgs,

                                        Type/*!*/ formalResult,

                                        List<Type>/*!*/ actualArgs) {

@@ -594,7 +594,7 @@ namespace Microsoft.Boogie {
       Type/*!*/ res = formalResult.Substitute(subst);

       Contract.Assert(res != null);

       // all type parameters have to be substituted with concrete types

-      TypeVariableSeq/*!*/ resFreeVars = res.FreeVariables;

+      List<TypeVariable>/*!*/ resFreeVars = res.FreeVariables;

       Contract.Assert(resFreeVars != null);

       Contract.Assert(Contract.ForAll(0, typeParams.Count, var => !resFreeVars.Contains(typeParams[var])));

       return res;

@@ -602,14 +602,14 @@ namespace Microsoft.Boogie {
 

 #if OLD_UNIFICATION

     public static IDictionary<TypeVariable!, Type!>!

-                  InferTypeParameters(TypeVariableSeq! typeParams,

+                  InferTypeParameters(List<TypeVariable>! typeParams,

                                       List<Type>! formalArgs,

                                       List<Type>! actualArgs)

       {

  Contract.Requires(formalArgs.Length == actualArgs.Length);

       

-      TypeVariableSeq! boundVarSeq0 = new TypeVariableSeq ();

-      TypeVariableSeq! boundVarSeq1 = new TypeVariableSeq ();

+      List<TypeVariable>! boundVarSeq0 = new List<TypeVariable> ();

+      List<TypeVariable>! boundVarSeq1 = new List<TypeVariable> ();

       Dictionary<TypeVariable!, Type!>! subst = new Dictionary<TypeVariable!, Type!>();

 

       for (int i = 0; i < formalArgs.Length; ++i) {

@@ -634,7 +634,7 @@ namespace Microsoft.Boogie {
     /// (and only does arguments, not results; and takes actuals as List<Type>, not List<Expr>)

     /// </summary>

     public static IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/

-                  InferTypeParameters(TypeVariableSeq/*!*/ typeParams,

+                  InferTypeParameters(List<TypeVariable>/*!*/ typeParams,

                                       List<Type>/*!*/ formalArgs,

                                       List<Type>/*!*/ actualArgs) {

       Contract.Requires(typeParams != null);

@@ -670,7 +670,7 @@ namespace Microsoft.Boogie {
 

     //-----------  Helper methods to deal with bound type variables  ---------------

 

-    public static void EmitOptionalTypeParams(TokenTextWriter stream, TypeVariableSeq typeParams) {

+    public static void EmitOptionalTypeParams(TokenTextWriter stream, List<TypeVariable> typeParams) {

       Contract.Requires(typeParams != null);

       Contract.Requires(stream != null);

       if (typeParams.Count > 0) {

@@ -681,23 +681,23 @@ namespace Microsoft.Boogie {
     }

 

     // Sort the type parameters according to the order of occurrence in the argument types

-    public static TypeVariableSeq/*!*/ SortTypeParams(TypeVariableSeq/*!*/ typeParams, List<Type>/*!*/ argumentTypes, Type resultType) {

+    public static List<TypeVariable>/*!*/ SortTypeParams(List<TypeVariable>/*!*/ typeParams, List<Type>/*!*/ argumentTypes, Type resultType) {

       Contract.Requires(typeParams != null);

       Contract.Requires(argumentTypes != null);

-      Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);

+      Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);

 

-      Contract.Ensures(Contract.Result<TypeVariableSeq>().Count == typeParams.Count);

+      Contract.Ensures(Contract.Result<List<TypeVariable>>().Count == typeParams.Count);

       if (typeParams.Count == 0) {

         return typeParams;

       }

 

-      TypeVariableSeq freeVarsInUse = FreeVariablesIn(argumentTypes);

+      List<TypeVariable> freeVarsInUse = FreeVariablesIn(argumentTypes);

       if (resultType != null) {

         freeVarsInUse.AppendWithoutDups(resultType.FreeVariables);

       }

       // "freeVarsInUse" is already sorted, but it may contain type variables not in "typeParams".

       // So, project "freeVarsInUse" onto "typeParams":

-      TypeVariableSeq sortedTypeParams = new TypeVariableSeq();

+      List<TypeVariable> sortedTypeParams = new List<TypeVariable>();

       foreach (TypeVariable/*!*/ var in freeVarsInUse) {

         Contract.Assert(var != null);

         if (typeParams.Contains(var)) {

@@ -717,7 +717,7 @@ namespace Microsoft.Boogie {
     // Return true if some type parameters appear only among "moreArgumentTypes" and

     // not in "argumentTypes".

     [Pure]

-    public static bool CheckBoundVariableOccurrences(TypeVariableSeq/*!*/ typeParams,

+    public static bool CheckBoundVariableOccurrences(List<TypeVariable>/*!*/ typeParams,

                                                      List<Type>/*!*/ argumentTypes,

                                                      List<Type> moreArgumentTypes,

                                                      IToken/*!*/ resolutionSubject,

@@ -728,8 +728,8 @@ namespace Microsoft.Boogie {
       Contract.Requires(resolutionSubject != null);

       Contract.Requires(subjectName != null);

       Contract.Requires(rc != null);

-      TypeVariableSeq freeVarsInArgs = FreeVariablesIn(argumentTypes);

-      TypeVariableSeq moFreeVarsInArgs = moreArgumentTypes == null ? null : FreeVariablesIn(moreArgumentTypes);

+      List<TypeVariable> freeVarsInArgs = FreeVariablesIn(argumentTypes);

+      List<TypeVariable> moFreeVarsInArgs = moreArgumentTypes == null ? null : FreeVariablesIn(moreArgumentTypes);

       bool someTypeParamsAppearOnlyAmongMo = false;

       foreach (TypeVariable/*!*/ var in typeParams) {

         Contract.Assert(var != null);

@@ -750,10 +750,10 @@ namespace Microsoft.Boogie {
     }

 

     [Pure]

-    public static TypeVariableSeq FreeVariablesIn(List<Type> arguments) {

+    public static List<TypeVariable> FreeVariablesIn(List<Type> arguments) {

       Contract.Requires(arguments != null);

-      Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);

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

+      Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);

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

       foreach (Type/*!*/ t in arguments) {

         Contract.Assert(t != null);

         res.AppendWithoutDups(t.FreeVariables);

@@ -772,9 +772,9 @@ namespace Microsoft.Boogie {
         throw new NotImplementedException();

       }

     }

-    public override TypeVariableSeq FreeVariables {

+    public override List<TypeVariable> FreeVariables {

       get {

-        Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);

+        Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);

         throw new NotImplementedException();

       }

     }

@@ -793,13 +793,13 @@ namespace Microsoft.Boogie {
       Contract.Requires(stream != null);

       throw new NotImplementedException();

     }

-    public override bool Equals(Type that, TypeVariableSeq thisBoundVariables, TypeVariableSeq thatBoundVariables) {

+    public override bool Equals(Type that, List<TypeVariable> thisBoundVariables, List<TypeVariable> thatBoundVariables) {

       Contract.Requires(that != null);

       Contract.Requires(thisBoundVariables != null);

       Contract.Requires(thatBoundVariables != null);

       throw new NotImplementedException();

     }

-    public override bool Unify(Type that, TypeVariableSeq unifiableVariables, IDictionary<TypeVariable, Type> unifier) {

+    public override bool Unify(Type that, List<TypeVariable> unifiableVariables, IDictionary<TypeVariable, Type> unifier) {

       Contract.Requires(that != null);

       Contract.Requires(unifiableVariables != null);

       Contract.Requires(cce.NonNullDictionaryAndValues(unifier));

@@ -819,7 +819,7 @@ namespace Microsoft.Boogie {
 

       throw new NotImplementedException();

     }

-    public override int GetHashCode(TypeVariableSeq boundVariables) {

+    public override int GetHashCode(List<TypeVariable> boundVariables) {

       Contract.Requires(boundVariables != null);

       throw new NotImplementedException();

     }

@@ -896,7 +896,7 @@ namespace Microsoft.Boogie {
     }

 

     [Pure]

-    public override bool Equals(Type that, TypeVariableSeq thisBoundVariables, TypeVariableSeq thatBoundVariables) {

+    public override bool Equals(Type that, List<TypeVariable> thisBoundVariables, List<TypeVariable> thatBoundVariables) {

       //Contract.Requires(thatBoundVariables != null);

       //Contract.Requires(thisBoundVariables != null);

       //Contract.Requires(that != null);

@@ -905,7 +905,7 @@ namespace Microsoft.Boogie {
 

     //-----------  Unification of types  -----------

 

-    public override bool Unify(Type that, TypeVariableSeq unifiableVariables, IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier) {

+    public override bool Unify(Type that, List<TypeVariable> unifiableVariables, IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier) {

       //Contract.Requires(unifiableVariables != null);

       //Contract.Requires(that != null);

       //Contract.Requires(cce.NonNullElements(unifier));

@@ -922,9 +922,9 @@ namespace Microsoft.Boogie {
 

 #if OLD_UNIFICATION

     public override void Unify(Type! that,

-                               TypeVariableSeq! unifiableVariables,

-                               TypeVariableSeq! thisBoundVariables,

-                               TypeVariableSeq! thatBoundVariables,

+                               List<TypeVariable>! unifiableVariables,

+                               List<TypeVariable>! thisBoundVariables,

+                               List<TypeVariable>! thatBoundVariables,

                                IDictionary<TypeVariable!, Type!>! result) {

       that = that.Expanded;

       if (that is TypeVariable) {

@@ -947,7 +947,7 @@ namespace Microsoft.Boogie {
     //-----------  Hashcodes  ----------------------------------

 

     [Pure]

-    public override int GetHashCode(TypeVariableSeq boundVariables) {

+    public override int GetHashCode(List<TypeVariable> boundVariables) {

       //Contract.Requires(boundVariables != null);

       return this.T.GetHashCode();

     }

@@ -962,11 +962,11 @@ namespace Microsoft.Boogie {
     }

 

     // determine the free variables in a type, in the order in which the variables occur

-    public override TypeVariableSeq/*!*/ FreeVariables {

+    public override List<TypeVariable>/*!*/ FreeVariables {

       get {

-        Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);

+        Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);

 

-        return new TypeVariableSeq();  // basic type are closed

+        return new List<TypeVariable>();  // basic type are closed

       }

     }

 

@@ -1059,8 +1059,8 @@ namespace Microsoft.Boogie {
 

     [Pure]

     public override bool Equals(Type/*!*/ that,

-                                TypeVariableSeq/*!*/ thisBoundVariables,

-                                TypeVariableSeq/*!*/ thatBoundVariables) {

+                                List<TypeVariable>/*!*/ thisBoundVariables,

+                                List<TypeVariable>/*!*/ thatBoundVariables) {

       //Contract.Requires(thisBoundVariables != null);

       //Contract.Requires(thatBoundVariables != null);

       //Contract.Requires(that != null);

@@ -1071,7 +1071,7 @@ namespace Microsoft.Boogie {
     //-----------  Unification of types  -----------

 

     public override bool Unify(Type/*!*/ that,

-                               TypeVariableSeq/*!*/ unifiableVariables,

+                               List<TypeVariable>/*!*/ unifiableVariables,

       // an idempotent substitution that describes the

       // unification result up to a certain point

                                IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier) {

@@ -1088,9 +1088,9 @@ namespace Microsoft.Boogie {
 

 #if OLD_UNIFICATION

     public override void Unify(Type that,

-                               TypeVariableSeq! unifiableVariables,

-                               TypeVariableSeq! thisBoundVariables,

-                               TypeVariableSeq! thatBoundVariables,

+                               List<TypeVariable>! unifiableVariables,

+                               List<TypeVariable>! thisBoundVariables,

+                               List<TypeVariable>! thatBoundVariables,

                                IDictionary<TypeVariable!, Type!> result){

 Contract.Requires(result != null);

 Contract.Requires(that != null);

@@ -1115,7 +1115,7 @@ Contract.Requires(that != null);
     //-----------  Hashcodes  ----------------------------------

 

     [Pure]

-    public override int GetHashCode(TypeVariableSeq boundVariables) {

+    public override int GetHashCode(List<TypeVariable> boundVariables) {

       //Contract.Requires(boundVariables != null);

       return this.Bits.GetHashCode();

     }

@@ -1130,11 +1130,11 @@ Contract.Requires(that != null);
     }

 

     // determine the free variables in a type, in the order in which the variables occur

-    public override TypeVariableSeq/*!*/ FreeVariables {

+    public override List<TypeVariable>/*!*/ FreeVariables {

       get {

-        Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);

+        Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);

 

-        return new TypeVariableSeq();  // bitvector-type are closed

+        return new List<TypeVariable>();  // bitvector-type are closed

       }

     }

 

@@ -1225,8 +1225,8 @@ Contract.Requires(that != null);
 

     [Pure]

     public override bool Equals(Type that,

-                                TypeVariableSeq/*!*/ thisBoundVariables,

-                                TypeVariableSeq/*!*/ thatBoundVariables) {

+                                List<TypeVariable>/*!*/ thisBoundVariables,

+                                List<TypeVariable>/*!*/ thatBoundVariables) {

       //Contract.Requires(thisBoundVariables != null);

       //Contract.Requires(thatBoundVariables != null);

       //Contract.Requires(that != null);

@@ -1237,7 +1237,7 @@ Contract.Requires(that != null);
     //-----------  Unification of types  -----------

 

     public override bool Unify(Type that,

-                               TypeVariableSeq/*!*/ unifiableVariables,

+                               List<TypeVariable>/*!*/ unifiableVariables,

                                IDictionary<TypeVariable/*!*/, Type/*!*/> result) {

       //Contract.Requires(unifiableVariables != null);

       //Contract.Requires(cce.NonNullElements(result));

@@ -1250,9 +1250,9 @@ Contract.Requires(that != null);
 

 #if OLD_UNIFICATION

     public override void Unify(Type that,

-                               TypeVariableSeq! unifiableVariables,

-                               TypeVariableSeq! thisBoundVariables,

-                               TypeVariableSeq! thatBoundVariables,

+                               List<TypeVariable>! unifiableVariables,

+                               List<TypeVariable>! thisBoundVariables,

+                               List<TypeVariable>! thatBoundVariables,

                                IDictionary<TypeVariable!, Type!> result){

 Contract.Requires(result != null);

 Contract.Requires(that != null);

@@ -1274,7 +1274,7 @@ Contract.Requires(that != null);
     //-----------  Hashcodes  ----------------------------------

 

     [Pure]

-    public override int GetHashCode(TypeVariableSeq boundVariables) {

+    public override int GetHashCode(List<TypeVariable> boundVariables) {

       //Contract.Requires(boundVariables != null);

       {

         Contract.Assert(false);

@@ -1362,11 +1362,11 @@ Contract.Requires(that != null);
       return resolvedArgs;

     }

 

-    public override TypeVariableSeq/*!*/ FreeVariables {

+    public override List<TypeVariable>/*!*/ FreeVariables {

       get {

-        Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);

+        Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);

 

-        return new TypeVariableSeq();

+        return new List<TypeVariable>();

       }

     }

 

@@ -1451,8 +1451,8 @@ Contract.Requires(that != null);
 

     [Pure]

     public override bool Equals(Type that,

-                                TypeVariableSeq/*!*/ thisBoundVariables,

-                                TypeVariableSeq/*!*/ thatBoundVariables) {

+                                List<TypeVariable>/*!*/ thisBoundVariables,

+                                List<TypeVariable>/*!*/ thatBoundVariables) {

       //Contract.Requires(thisBoundVariables != null);

       //Contract.Requires(thatBoundVariables != null);

       //Contract.Requires(that != null);

@@ -1471,7 +1471,7 @@ Contract.Requires(that != null);
     //-----------  Unification of types  -----------

 

     public override bool Unify(Type/*!*/ that,

-                               TypeVariableSeq/*!*/ unifiableVariables,

+                               List<TypeVariable>/*!*/ unifiableVariables,

       // an idempotent substitution that describes the

       // unification result up to a certain point

                                IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier) {

@@ -1540,9 +1540,9 @@ Contract.Requires(that != null);
 

 #if OLD_UNIFICATION

     public override void Unify(Type that,

-                               TypeVariableSeq! unifiableVariables,

-                               TypeVariableSeq! thisBoundVariables,

-                               TypeVariableSeq! thatBoundVariables,

+                               List<TypeVariable>! unifiableVariables,

+                               List<TypeVariable>! thisBoundVariables,

+                               List<TypeVariable>! thatBoundVariables,

                                IDictionary<TypeVariable!, Type!> result){

 Contract.Requires(result != null);

 Contract.Requires(that != null);

@@ -1551,7 +1551,7 @@ Contract.Requires(that != null);
       if (thisIndex == -1) {

         // this is not a bound variable and can possibly be matched on that

         // that must not contain any bound variables

-        TypeVariableSeq! thatFreeVars = that.FreeVariables;

+        List<TypeVariable>! thatFreeVars = that.FreeVariables;

         if (Contract.Exists(thatBoundVariables, var=> thatFreeVars.Has(var)))

           throw UNIFICATION_FAILED;

 

@@ -1607,7 +1607,7 @@ Contract.Requires(that != null);
     //-----------  Hashcodes  ----------------------------------

 

     [Pure]

-    public override int GetHashCode(TypeVariableSeq boundVariables) {

+    public override int GetHashCode(List<TypeVariable> boundVariables) {

       //Contract.Requires(boundVariables != null);

       int thisIndex = boundVariables.LastIndexOf(this);

       if (thisIndex == -1)

@@ -1633,10 +1633,10 @@ Contract.Requires(that != null);
       return this;

     }

 

-    public override TypeVariableSeq/*!*/ FreeVariables {

+    public override List<TypeVariable>/*!*/ FreeVariables {

       get {

-        Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);

-        return new TypeVariableSeq(this);

+        Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);

+        return new List<TypeVariable> { this };

       }

     }

 

@@ -1755,8 +1755,8 @@ Contract.Requires(that != null);
 

     [Pure]

     public override bool Equals(Type that,

-                                TypeVariableSeq/*!*/ thisBoundVariables,

-                                TypeVariableSeq/*!*/ thatBoundVariables) {

+                                List<TypeVariable>/*!*/ thisBoundVariables,

+                                List<TypeVariable>/*!*/ thatBoundVariables) {

       //Contract.Requires(thisBoundVariables != null);

       //Contract.Requires(thatBoundVariables != null);

       //Contract.Requires(that != null);

@@ -1783,7 +1783,7 @@ Contract.Requires(that != null);
     }

 

     public override bool Unify(Type that,

-                               TypeVariableSeq/*!*/ unifiableVariables,

+                               List<TypeVariable>/*!*/ unifiableVariables,

                                IDictionary<TypeVariable/*!*/, Type/*!*/> result) {

       //Contract.Requires(cce.NonNullElements(result));

       //Contract.Requires(unifiableVariables != null);

@@ -1816,7 +1816,7 @@ Contract.Requires(that != null);
     //-----------  Hashcodes  ----------------------------------

 

     [Pure]

-    public override int GetHashCode(TypeVariableSeq boundVariables) {

+    public override int GetHashCode(List<TypeVariable> boundVariables) {

       //Contract.Requires(boundVariables != null);

       Type p = ProxyFor;

       if (p != null) {

@@ -1853,15 +1853,15 @@ Contract.Requires(that != null);
       }

     }

 

-    public override TypeVariableSeq/*!*/ FreeVariables {

+    public override List<TypeVariable>/*!*/ FreeVariables {

       get {

-        Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);

+        Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);

 

         Type p = ProxyFor;

         if (p != null) {

           return p.FreeVariables;

         } else {

-          return new TypeVariableSeq();

+          return new List<TypeVariable>();

         }

       }

     }

@@ -2123,7 +2123,7 @@ Contract.Requires(that != null);
     //-----------  Unification of types  -----------

 

     public override bool Unify(Type that,

-                               TypeVariableSeq unifiableVariables,

+                               List<TypeVariable> unifiableVariables,

                                IDictionary<TypeVariable, Type> result) {

       //Contract.Requires(cce.NonNullElements(result));

       //Contract.Requires(unifiableVariables != null);

@@ -2300,7 +2300,7 @@ Contract.Requires(that != null);
       }

 

       public bool Unify(MapType that,

-                        TypeVariableSeq/*!*/ unifiableVariables,

+                        List<TypeVariable>/*!*/ unifiableVariables,

                         IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ result) {

         Contract.Requires(unifiableVariables != null);

         Contract.Requires(cce.NonNullDictionaryAndValues(result));

@@ -2338,7 +2338,7 @@ Contract.Requires(that != null);
       Type f = ProxyFor;

       MapType mf = f as MapType;

       if (mf != null) {

-        bool success = c.Unify(mf, new TypeVariableSeq(), new Dictionary<TypeVariable/*!*/, Type/*!*/>());

+        bool success = c.Unify(mf, new List<TypeVariable>(), new Dictionary<TypeVariable/*!*/, Type/*!*/>());

         Contract.Assert(success);

         return;

       }

@@ -2437,7 +2437,7 @@ Contract.Requires(that != null);
     //-----------  Unification of types  -----------

 

     public override bool Unify(Type/*!*/ that,

-                               TypeVariableSeq/*!*/ unifiableVariables,

+                               List<TypeVariable>/*!*/ unifiableVariables,

                                IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ result) {

       //Contract.Requires(that != null);

       //Contract.Requires(unifiableVariables != null);

@@ -2626,8 +2626,8 @@ Contract.Requires(that != null);
 

     [Pure]

     public override bool Equals(Type/*!*/ that,

-                                TypeVariableSeq/*!*/ thisBoundVariables,

-                                TypeVariableSeq/*!*/ thatBoundVariables) {

+                                List<TypeVariable>/*!*/ thisBoundVariables,

+                                List<TypeVariable>/*!*/ thatBoundVariables) {

       //Contract.Requires(that != null);

       //Contract.Requires(thisBoundVariables != null);

       //Contract.Requires(thatBoundVariables != null);

@@ -2646,7 +2646,7 @@ Contract.Requires(that != null);
     //-----------  Unification of types  -----------

 

     public override bool Unify(Type/*!*/ that,

-                               TypeVariableSeq/*!*/ unifiableVariables,

+                               List<TypeVariable>/*!*/ unifiableVariables,

                                IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ result) {

       //Contract.Requires(that != null);

       //Contract.Requires(unifiableVariables != null);

@@ -2656,9 +2656,9 @@ Contract.Requires(that != null);
 

 #if OLD_UNIFICATION

     public override void Unify(Type! that,

-                               TypeVariableSeq! unifiableVariables,

-                               TypeVariableSeq! thisBoundVariables,

-                               TypeVariableSeq! thatBoundVariables,

+                               List<TypeVariable>! unifiableVariables,

+                               List<TypeVariable>! thisBoundVariables,

+                               List<TypeVariable>! thatBoundVariables,

                                IDictionary<TypeVariable!, Type!>! result) {

       ExpandedType.Unify(that, unifiableVariables,

                          thisBoundVariables, thatBoundVariables, result);

@@ -2685,7 +2685,7 @@ Contract.Requires(that != null);
     //-----------  Hashcodes  ----------------------------------

 

     [Pure]

-    public override int GetHashCode(TypeVariableSeq boundVariables) {

+    public override int GetHashCode(List<TypeVariable> boundVariables) {

       //Contract.Requires(boundVariables != null);

       return ExpandedType.GetHashCode(boundVariables);

     }

@@ -2711,9 +2711,9 @@ Contract.Requires(that != null);
       return new TypeSynonymAnnotation(tok, Decl, resolvedArgs);

     }

 

-    public override TypeVariableSeq/*!*/ FreeVariables {

+    public override List<TypeVariable>/*!*/ FreeVariables {

       get {

-        Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);

+        Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);

 

         return ExpandedType.FreeVariables;

       }

@@ -2886,8 +2886,8 @@ Contract.Requires(that != null);
 

     [Pure]

     public override bool Equals(Type/*!*/ that,

-                                TypeVariableSeq/*!*/ thisBoundVariables,

-                                TypeVariableSeq/*!*/ thatBoundVariables) {

+                                List<TypeVariable>/*!*/ thisBoundVariables,

+                                List<TypeVariable>/*!*/ thatBoundVariables) {

       that = TypeProxy.FollowProxy(that.Expanded);

       CtorType thatCtorType = that as CtorType;

       if (thatCtorType == null || !this.Decl.Equals(thatCtorType.Decl))

@@ -2903,7 +2903,7 @@ Contract.Requires(that != null);
     //-----------  Unification of types  -----------

 

     public override bool Unify(Type/*!*/ that,

-                               TypeVariableSeq/*!*/ unifiableVariables,

+                               List<TypeVariable>/*!*/ unifiableVariables,

                                IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ result) {

       that = that.Expanded;

       if (that is TypeProxy || that is TypeVariable)

@@ -2922,9 +2922,9 @@ Contract.Requires(that != null);
 

 #if OLD_UNIFICATION

     public override void Unify(Type! that,

-                               TypeVariableSeq! unifiableVariables,

-                               TypeVariableSeq! thisBoundVariables,

-                               TypeVariableSeq! thatBoundVariables,

+                               List<TypeVariable>! unifiableVariables,

+                               List<TypeVariable>! thisBoundVariables,

+                               List<TypeVariable>! thatBoundVariables,

                                IDictionary<TypeVariable!, Type!>! result) {

       that = that.Expanded;

       if (that is TypeVariable) {

@@ -2961,7 +2961,7 @@ Contract.Requires(that != null);
     //-----------  Hashcodes  ----------------------------------

 

     [Pure]

-    public override int GetHashCode(TypeVariableSeq boundVariables) {

+    public override int GetHashCode(List<TypeVariable> boundVariables) {

       //Contract.Requires(boundVariables != null);

       int res = 1637643879 * Decl.GetHashCode();

       foreach (Type/*!*/ t in Arguments) {

@@ -3015,9 +3015,9 @@ Contract.Requires(that != null);
       return new CtorType(tok, Decl, resolvedArgs);

     }

 

-    public override TypeVariableSeq/*!*/ FreeVariables {

+    public override List<TypeVariable>/*!*/ FreeVariables {

       get {

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

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

         foreach (Type/*!*/ t in Arguments) {

           Contract.Assert(t != null);

           res.AppendWithoutDups(t.FreeVariables);

@@ -3062,7 +3062,7 @@ Contract.Requires(that != null);
   public class MapType : Type {

     // an invariant is that each of the type parameters has to occur as

     // free variable in at least one of the arguments

-    public readonly TypeVariableSeq/*!*/ TypeParameters;

+    public readonly List<TypeVariable>/*!*/ TypeParameters;

     public readonly List<Type>/*!*/ Arguments;

     public Type/*!*/ Result;

     [ContractInvariantMethod]

@@ -3073,7 +3073,7 @@ Contract.Requires(that != null);
     }

 

 

-    public MapType(IToken/*!*/ token, TypeVariableSeq/*!*/ typeParameters, List<Type>/*!*/ arguments, Type/*!*/ result)

+    public MapType(IToken/*!*/ token, List<TypeVariable>/*!*/ typeParameters, List<Type>/*!*/ arguments, Type/*!*/ result)

       : base(token) {

       Contract.Requires(token != null);

       Contract.Requires(typeParameters != null);

@@ -3101,7 +3101,7 @@ Contract.Requires(that != null);
           newVarMap.Add(p);

       }

 

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

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

       foreach (TypeVariable/*!*/ var in TypeParameters) {

         Contract.Assert(var != null);

         TypeVariable/*!*/ newVar = new TypeVariable(var.tok, var.Name);

@@ -3123,7 +3123,7 @@ Contract.Requires(that != null);
 

     public override Type CloneUnresolved() {

       Contract.Ensures(Contract.Result<Type>() != null);

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

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

       foreach (TypeVariable/*!*/ var in TypeParameters) {

         Contract.Assert(var != null);

         TypeVariable/*!*/ newVar = new TypeVariable(var.tok, var.Name);

@@ -3146,8 +3146,8 @@ Contract.Requires(that != null);
 

     [Pure]

     public override bool Equals(Type/*!*/ that,

-                                TypeVariableSeq/*!*/ thisBoundVariables,

-                                TypeVariableSeq/*!*/ thatBoundVariables) {

+                                List<TypeVariable>/*!*/ thisBoundVariables,

+                                List<TypeVariable>/*!*/ thatBoundVariables) {

       that = TypeProxy.FollowProxy(that.Expanded);

       MapType thatMapType = that as MapType;

       if (thatMapType == null ||

@@ -3189,7 +3189,7 @@ Contract.Requires(that != null);
     //-----------  Unification of types  -----------

 

     public override bool Unify(Type/*!*/ that,

-                               TypeVariableSeq/*!*/ unifiableVariables,

+                               List<TypeVariable>/*!*/ unifiableVariables,

                                IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ result) {

       that = that.Expanded;

       if (that is TypeProxy || that is TypeVariable)

@@ -3206,7 +3206,7 @@ Contract.Requires(that != null);
         new Dictionary<TypeVariable/*!*/, Type/*!*/>();

       Dictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst1 =

         new Dictionary<TypeVariable/*!*/, Type/*!*/>();

-      TypeVariableSeq freshies = new TypeVariableSeq();

+      List<TypeVariable> freshies = new List<TypeVariable>();

       for (int i = 0; i < this.TypeParameters.Count; i++) {

         TypeVariable tp0 = this.TypeParameters[i];

         TypeVariable tp1 = thatMapType.TypeParameters[i];

@@ -3230,7 +3230,7 @@ Contract.Requires(that != null);
       if (good && freshies.Count != 0) {

         // This is done by looking for occurrences of the fresh variables in the

         // non-substituted types ...

-        TypeVariableSeq freeVars = this.FreeVariables;

+        List<TypeVariable> freeVars = this.FreeVariables;

         foreach (TypeVariable fr in freshies)

           if (freeVars.Contains(fr)) {

             return false;

@@ -3257,9 +3257,9 @@ Contract.Requires(that != null);
 

 #if OLD_UNIFICATION

     public override void Unify(Type! that,

-                               TypeVariableSeq! unifiableVariables,

-                               TypeVariableSeq! thisBoundVariables,

-                               TypeVariableSeq! thatBoundVariables,

+                               List<TypeVariable>! unifiableVariables,

+                               List<TypeVariable>! thisBoundVariables,

+                               List<TypeVariable>! thatBoundVariables,

                                IDictionary<TypeVariable!, Type!>! result) {

       that = that.Expanded;

       if (that is TypeVariable) {

@@ -3356,7 +3356,7 @@ Contract.Assert(var != null);
     //-----------  Hashcodes  ----------------------------------

 

     [Pure]

-    public override int GetHashCode(TypeVariableSeq boundVariables) {

+    public override int GetHashCode(List<TypeVariable> boundVariables) {

       //Contract.Requires(boundVariables != null);

       int res = 7643761 * TypeParameters.Count + 65121 * Arguments.Count;

 

@@ -3424,7 +3424,7 @@ Contract.Assert(var != null);
                                       rc);

 

         // sort the type parameters so that they are bound in the order of occurrence

-        TypeVariableSeq/*!*/ sortedTypeParams = SortTypeParams(TypeParameters, resolvedArgs, resolvedResult);

+        List<TypeVariable>/*!*/ sortedTypeParams = SortTypeParams(TypeParameters, resolvedArgs, resolvedResult);

         Contract.Assert(sortedTypeParams != null);

         return new MapType(tok, sortedTypeParams, resolvedArgs, resolvedResult);

       } finally {

@@ -3432,9 +3432,9 @@ Contract.Assert(var != null);
       }

     }

 

-    public override TypeVariableSeq/*!*/ FreeVariables {

+    public override List<TypeVariable>/*!*/ FreeVariables {

       get {

-        TypeVariableSeq/*!*/ res = FreeVariablesIn(Arguments);

+        List<TypeVariable>/*!*/ res = FreeVariablesIn(Arguments);

         Contract.Assert(res != null);

         res.AppendWithoutDups(Result.FreeVariables);

         foreach (TypeVariable/*!*/ v in TypeParameters) {

@@ -3584,7 +3584,7 @@ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
       this.Instantiations = instantiations;

     }

 

-    public static TypeParamInstantiation/*!*/ From(TypeVariableSeq typeParams, List<Type/*!*/>/*!*/ actualTypeParams) {

+    public static TypeParamInstantiation/*!*/ From(List<TypeVariable> typeParams, List<Type/*!*/>/*!*/ actualTypeParams) {

       Contract.Requires(cce.NonNullElements(actualTypeParams));

       Contract.Requires(typeParams != null);

       Contract.Requires(typeParams.Count == actualTypeParams.Count);

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> ();

diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs
index a461db22..9b8a09c1 100644
--- a/Source/Core/LambdaHelper.cs
+++ b/Source/Core/LambdaHelper.cs
@@ -100,9 +100,9 @@ namespace Microsoft.Boogie {
           List<Expr> callArgs = new List<Expr>();

           List<Expr> axCallArgs = new List<Expr>();

           List<Variable> dummies = new List<Variable>(lambda.Dummies);

-          TypeVariableSeq freeTypeVars = new TypeVariableSeq();

+          List<TypeVariable> freeTypeVars = new List<TypeVariable>();

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

-          TypeVariableSeq freshTypeVars = new TypeVariableSeq();  // these are only used in the lambda@n function's definition

+          List<TypeVariable> freshTypeVars = new List<TypeVariable>();  // these are only used in the lambda@n function's definition

           foreach (object o in freeVars) {

             // 'o' is either a Variable or a TypeVariable.  Since the lambda desugaring happens only

             // at the outermost level of a program (where there are no mutable variables) and, for

@@ -147,7 +147,7 @@ namespace Microsoft.Boogie {
           NAryExpr select = Expr.Select(axcall, selectArgs);

           select.Type = lambda.Body.Type;

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

-          TypeVariableSeq forallTypeVariables = new TypeVariableSeq();

+          List<TypeVariable> forallTypeVariables = new List<TypeVariable>();

           foreach (TypeVariable/*!*/ tp in lambda.TypeParameters) {

             Contract.Assert(tp != null);

             selectTypeParamActuals.Add(tp);

diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs
index 5b9aee5f..c8815575 100644
--- a/Source/Core/LinearSets.cs
+++ b/Source/Core/LinearSets.cs
@@ -404,7 +404,7 @@ namespace Microsoft.Boogie
                       Token.NoToken,

                       new TypedIdent(Token.NoToken, 

                         domainName + "_in",

-                        new MapType(Token.NoToken, new TypeVariableSeq(), 

+                        new MapType(Token.NoToken, new List<TypeVariable>(), 

                           new List<Type> { domain.elementType }, Type.Bool)), true);

                     impl.InParams.Add(f);

                     domainNameToInputVar[domainName] = f;

@@ -523,7 +523,7 @@ namespace Microsoft.Boogie
                 {

                     proc.Requires.Add(new Requires(true, DisjointnessExpr(domainName, domainNameToInputScope[domainName])));

                     var domain = linearDomains[domainName];

-                    Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type> { domain.elementType }, Type.Bool)), true);

+                    Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);

                     proc.InParams.Add(f);

                     domainNameToOutputScope[domainName].Add(f);

                     proc.Ensures.Add(new Ensures(true, DisjointnessExpr(domainName, domainNameToOutputScope[domainName])));

@@ -573,7 +573,7 @@ namespace Microsoft.Boogie
         public Expr DisjointnessExpr(string domainName, HashSet<Variable> scope)

         {

             LinearDomain domain = linearDomains[domainName];

-            BoundVariable partition = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("partition_{0}", domainName), new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type> { domain.elementType }, Microsoft.Boogie.Type.Int)));

+            BoundVariable partition = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("partition_{0}", domainName), new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Microsoft.Boogie.Type.Int)));

             Expr disjointExpr = Expr.True;

             int count = 0;

             foreach (Variable v in scope)

@@ -604,8 +604,8 @@ namespace Microsoft.Boogie
             this.elementType = elementType;

             this.axioms = new List<Axiom>();

 

-            MapType mapTypeBool = new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type> { this.elementType }, Type.Bool);

-            MapType mapTypeInt = new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type> { this.elementType }, Type.Int);

+            MapType mapTypeBool = new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { this.elementType }, Type.Bool);

+            MapType mapTypeInt = new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { this.elementType }, Type.Int);

             this.mapOrBool = new Function(Token.NoToken, domainName + "_linear_MapOr",

                                           new List<Variable> { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true),

                                                           new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool), true) },

@@ -627,7 +627,7 @@ namespace Microsoft.Boogie
                 var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Or,

                                           new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { aie, xie } ),

                                           new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { bie, xie} ));

-                var axiomExpr = new ForallExpr(Token.NoToken, new TypeVariableSeq(), new List<Variable> { a, b }, null, 

+                var axiomExpr = new ForallExpr(Token.NoToken, new List<TypeVariable>(), new List<Variable> { a, b }, null, 

                                                new Trigger(Token.NoToken, true, new List<Expr> { mapApplTerm }), 

                                                new ForallExpr(Token.NoToken, new List<Variable> { x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));

                 axiomExpr.Typecheck(new TypecheckingContext(null));

@@ -655,7 +655,7 @@ namespace Microsoft.Boogie
                 var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Imp,

                                           new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { aie, xie }),

                                           new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { bie, xie }));

-                var axiomExpr = new ForallExpr(Token.NoToken, new TypeVariableSeq(), new List<Variable> { a, b }, null,

+                var axiomExpr = new ForallExpr(Token.NoToken, new List<TypeVariable>(), new List<Variable> { a, b }, null,

                                                new Trigger(Token.NoToken, true, new List<Expr> { mapApplTerm }), 

                                                new ForallExpr(Token.NoToken, new List<Variable> { x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));

                 axiomExpr.Typecheck(new TypecheckingContext(null));

@@ -706,7 +706,7 @@ namespace Microsoft.Boogie
                 var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Eq,

                                           new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { aie, xie }),

                                           new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { bie, xie }));

-                var axiomExpr = new ForallExpr(Token.NoToken, new TypeVariableSeq(), new List<Variable> { a, b }, null, 

+                var axiomExpr = new ForallExpr(Token.NoToken, new List<TypeVariable>(), new List<Variable> { a, b }, null, 

                                                new Trigger(Token.NoToken, true, new List<Expr> { mapApplTerm }), 

                                                new ForallExpr(Token.NoToken, new List<Variable> { x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));

                 axiomExpr.Typecheck(new TypecheckingContext(null));

diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index 90cfce97..eaafafc5 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -168,7 +168,7 @@ namespace Microsoft.Boogie
             foreach (string domainName in linearTypechecker.linearDomains.Keys)

             {

                 var domain = linearTypechecker.linearDomains[domainName];

-                Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type> { domain.elementType }, Type.Bool)), true);

+                Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);

                 inputs.Add(f);

             }

             foreach (IdentifierExpr ie in globalMods)

@@ -176,7 +176,7 @@ namespace Microsoft.Boogie
                 Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true);

                 inputs.Add(f);

             }

-            yieldProc = new Procedure(Token.NoToken, "og_yield", new TypeVariableSeq(), inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());

+            yieldProc = new Procedure(Token.NoToken, "og_yield", new List<TypeVariable>(), inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());

             yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));

         }

 

@@ -312,7 +312,7 @@ namespace Microsoft.Boogie
                 callCmd = callCmd.InParallelWith;

             }

 

-            Procedure proc = new Procedure(Token.NoToken, procName, new TypeVariableSeq(), inParams, outParams, requiresSeq, ieSeq, ensuresSeq);

+            Procedure proc = new Procedure(Token.NoToken, procName, new List<TypeVariable>(), inParams, outParams, requiresSeq, ieSeq, ensuresSeq);

             asyncAndParallelCallDesugarings[procName] = proc;

             return proc;

         }

@@ -727,7 +727,7 @@ namespace Microsoft.Boogie
             foreach (string domainName in linearTypechecker.linearDomains.Keys)

             {

                 var domain = linearTypechecker.linearDomains[domainName];

-                Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type> { domain.elementType }, Type.Bool)), true);

+                Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);

                 inputs.Add(f);

             }

             foreach (IdentifierExpr ie in globalMods)

@@ -761,7 +761,7 @@ namespace Microsoft.Boogie
             }

             blocks.Insert(0, new Block(Token.NoToken, "enter", new List<Cmd>(), transferCmd));

             

-            var yieldImpl = new Implementation(Token.NoToken, yieldProc.Name, new TypeVariableSeq(), inputs, new List<Variable>(), new List<Variable>(), blocks);

+            var yieldImpl = new Implementation(Token.NoToken, yieldProc.Name, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks);

             yieldImpl.Proc = yieldProc;

             yieldImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));

             program.TopLevelDeclarations.Add(yieldProc);

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 3064ae0f..9dc4a70e 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -324,7 +324,7 @@ private class BvBounds : Expr {
 		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;

@@ -468,7 +468,7 @@ private class BvBounds : Expr {
 

 	void 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>();

@@ -500,7 +500,7 @@ private class BvBounds : Expr {
 

 	void 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;

@@ -708,7 +708,7 @@ private class BvBounds : Expr {
 		IToken/*!*/ nnTok;

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

 		Bpl.Type/*!*/ result;

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

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

 		

 		if (la.kind == 19) {

 			TypeParams(out nnTok, out typeParameters);

@@ -725,13 +725,13 @@ private class BvBounds : Expr {
 		

 	}

 

-	void TypeParams(out IToken/*!*/ tok, out Bpl.TypeVariableSeq/*!*/ typeParams) {

+	void TypeParams(out IToken/*!*/ tok, out List<TypeVariable>/*!*/ typeParams) {

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

 		Expect(19);

 		tok = t;  

 		Idents(out typeParamToks);

 		Expect(20);

-		typeParams = new TypeVariableSeq ();

+		typeParams = new List<TypeVariable> ();

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

 		 Contract.Assert(id != null);

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

@@ -827,7 +827,7 @@ private class BvBounds : Expr {
 			synonym = true; 

 		}

 		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));}

@@ -848,10 +848,10 @@ private class BvBounds : Expr {
 		}

 	}

 

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

+	void 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; 

 		while (la.kind == 27) {

 			Attribute(ref kv);

@@ -1689,7 +1689,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 	void 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;

@@ -1850,10 +1850,10 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 		} else SynErr(126);

 	}

 

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

+	void 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> ();

diff --git a/Source/Core/TypeAmbiguitySeeker.cs b/Source/Core/TypeAmbiguitySeeker.cs
index ecb1e418..dac8ceb2 100644
--- a/Source/Core/TypeAmbiguitySeeker.cs
+++ b/Source/Core/TypeAmbiguitySeeker.cs
@@ -92,7 +92,7 @@ namespace Microsoft.Boogie {
       if (node.ProxyFor != null)

         return base.VisitMapTypeProxy(node);

 

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

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

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

       for (int i = 0; i < node.Arity; ++i) {

         TypeVariable/*!*/ param = new TypeVariable(Token.NoToken, "arg" + i);