Merge

2 files changed, 2 insertions, 2 deletions

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) &&