From c16176d2993c2df6b8b1b136c28a76cac3165b57 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Sat, 26 Mar 2011 01:58:19 +0000
Subject: Dafny: compile quantifiers Dafny: allow {:induction} attribute to
 take an explicit list of bound variables on which to apply induction Dafny:
 split expressions when proving function postconditions Boogie and BVD:
 updated copyright year ranges

---
 Source/VCExpr/TypeErasure.cs | 1 +
 1 file changed, 1 insertion(+)

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

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index 616575db..93adec82 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -327,6 +327,7 @@ namespace Microsoft.Boogie.TypeErasure {
     public readonly Type/*!*/ T;
 
     public abstract Type/*!*/ TypeAfterErasure(Type/*!*/ type);
+    [Pure]
     public abstract bool UnchangedType(Type/*!*/ type);
 
     ///////////////////////////////////////////////////////////////////////////
-- 
cgit v1.2.3