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/VSI-Benchmarks/b4.dfy | 2 +-
 Test/VSI-Benchmarks/b8.dfy | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'Test/VSI-Benchmarks')

diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index b70ff4d0..76e1ffa7 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -14,7 +14,7 @@
 // that the specification can use mathematical sequences while the
 // implementation uses a linked list.
 
-class Map<Key,Value> {
+class Map<Key(==),Value> {
   ghost var Keys: seq<Key>;
   ghost var Values: seq<Value>;
   ghost var Repr: set<object>;
diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index 383bccfd..2149df25 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -250,7 +250,7 @@ class WriterStream {
   
   
   
-class Map<Key,Value> {
+class Map<Key(==),Value> {
   var keys: seq<Key>;
   var values: seq<Value>;
   
-- 
cgit v1.2.3