From 7c6cfaa37c96349fda99823c6f98a576dba194b4 Mon Sep 17 00:00:00 2001
From: Unknown <leino@LEINO6.redmond.corp.microsoft.com>
Date: Thu, 21 Jun 2012 19:16:05 -0700
Subject: Dafny: Since it's no longer true that all types support equality at
 run-time (in particular, codatatypes), Dafny needs to check this.  In these
 changes, Dafny supports the "(==)" suffix to type parameters, infers that
 suffix in some cases, and enforces equality support in many places. 
 Refinement and datatypes still need more attention in the Dafny
 implementation.

---
 Test/dafny1/Celebrity.dfy   | 2 +-
 Test/dafny1/UltraFilter.dfy | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'Test/dafny1')

diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy
index 21b895aa..4c761671 100644
--- a/Test/dafny1/Celebrity.dfy
+++ b/Test/dafny1/Celebrity.dfy
@@ -10,7 +10,7 @@ static function IsCelebrity<Person>(c: Person, people: set<Person>): bool
 }
 
 method FindCelebrity0<Person>(people: set<Person>, ghost c: Person) returns (r: Person)
-  requires (exists c :: IsCelebrity(c, people));
+  requires exists c :: IsCelebrity(c, people);
   ensures r == c;
 {
   var cc; assume cc == c;  // this line essentially converts ghost c to non-ghost cc
diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy
index c8419890..c78d5e81 100644
--- a/Test/dafny1/UltraFilter.dfy
+++ b/Test/dafny1/UltraFilter.dfy
@@ -1,6 +1,6 @@
 // ultra filter
 
-class UltraFilter<G> {
+class UltraFilter<G(==)> {
   static function IsFilter(f: set<set<G>>, S: set<G>): bool
   {
     (forall A, B :: A in f && A <= B ==> B in f) &&
-- 
cgit v1.2.3