From dd8117ebb70bdb1531a35eb47f490929a5c658fb Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Sun, 7 Jun 2015 11:49:47 -0700
Subject: Fix the Seq#Contain axiom; it should talk about T, not ref.

---
 Binaries/DafnyPrelude.bpl | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Binaries')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 5ee8b845..ef6106e0 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -836,7 +836,7 @@ function Seq#Contains<T>(Seq T, T): bool;
 axiom (forall<T> s: Seq T, x: T :: { Seq#Contains(s,x) }
   Seq#Contains(s,x) <==>
     (exists i: int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && Seq#Index(s,i) == x));
-axiom (forall x: ref ::
+axiom (forall<T> x: T ::
   { Seq#Contains(Seq#Empty(), x) }
   !Seq#Contains(Seq#Empty(), x));
 
-- 
cgit v1.2.3