From 31c11cdcbcb3e82f4ed769de7e7d0d362f657a93 Mon Sep 17 00:00:00 2001
From: tabarbe <unknown>
Date: Fri, 20 Aug 2010 00:53:31 +0000
Subject: Boogie: Fixed some doubly-inherited-contract occurrences.

---
 Source/VCExpr/TypeErasure.cs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Source/VCExpr')

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index 5029ba53..f148dc79 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -655,10 +655,10 @@ Contract.Ensures(Contract.ValueAtReturn(out var) != null);
       }
       return res;
     }
-
+    [Pure]
     public Function CastTo(Type type) {
       Contract.Requires(type != null);
-      Contract.Requires((UnchangedType(type)));
+      Contract.Requires(UnchangedType(type));
       Contract.Ensures(Contract.Result<Function>() != null);
       return GetTypeCasts(type).CastFromU;
     }
-- 
cgit v1.2.3