From 350d32403f7441df525f871f3853ca9b660211fe Mon Sep 17 00:00:00 2001
From: Ally Donaldson <unknown>
Date: Mon, 22 Jul 2013 23:03:55 +0100
Subject: All ...Seq classes now gone

---
 Source/VCExpr/TypeErasure.cs | 17 +++--------------
 1 file changed, 3 insertions(+), 14 deletions(-)

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

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index f7860169..a25781af 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -40,7 +40,7 @@ namespace Microsoft.Boogie.TypeErasure {
                                    new TypedIdent(Token.NoToken, "res",
                                                    cce.NonNull(types)[types.Length - 1]),
                                    false);
-      return new Function(Token.NoToken, name, ToSeq(typeParams), args, result);
+      return new Function(Token.NoToken, name, new List<TypeVariable>(typeParams), args, result);
     }
 
     public static Function BoogieFunction(string name, params Type[] types) {
@@ -80,7 +80,7 @@ namespace Microsoft.Boogie.TypeErasure {
       return new List<T>(args);
     }
 
-    public static List<TypeVariable/*!*/>/*!*/ ToList(TypeVariableSeq seq) {
+    public static List<TypeVariable/*!*/>/*!*/ ToList(List<TypeVariable> seq) {
       Contract.Requires(seq != null);
       Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeVariable>>()));
       List<TypeVariable/*!*/>/*!*/ res = new List<TypeVariable/*!*/>(seq.Count);
@@ -91,17 +91,6 @@ namespace Microsoft.Boogie.TypeErasure {
       return res;
     }
 
-    public static TypeVariableSeq ToSeq(List<TypeVariable/*!*/>/*!*/ list) {
-      Contract.Requires(cce.NonNullElements(list));
-      Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);
-      TypeVariableSeq/*!*/ res = new TypeVariableSeq();
-      foreach (TypeVariable/*!*/ var in list) {
-        Contract.Assert(var != null);
-        res.Add(var);
-      }
-      return res;
-    }
-
     public static List<T>/*!*/ Intersect<T>(List<T> a, List<T> b) {
       Contract.Requires(b != null);
       Contract.Requires(a != null);
@@ -991,7 +980,7 @@ namespace Microsoft.Boogie.TypeErasure {
     }
 
     // the instantiations of inserted type variables, the order corresponds to the order in which "AbstractionVariable(int)" delivers variables
-    private Type/*!*/ ThinOutType(Type rawType, TypeVariableSeq boundTypeParams, List<Type> instantiations) {
+    private Type/*!*/ ThinOutType(Type rawType, List<TypeVariable> boundTypeParams, List<Type> instantiations) {
       Contract.Requires(instantiations != null);
       Contract.Requires(boundTypeParams != null);
       Contract.Requires(rawType != null);
-- 
cgit v1.2.3