Fix issue #71. When substitute the forall's variables for those of the

fn in fixupRevealLemma substitute the types as well.

1 files changed, 10 insertions, 0 deletions

diff --git a/Test/dafny4/Bug71.dfy b/Test/dafny4/Bug71.dfy
new file mode 100644
index 00000000..1c3fcf61
--- /dev/null
+++ b/Test/dafny4/Bug71.dfy
@@ -0,0 +1,10 @@
+// RUN: %dafny /compile:0 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+function{:opaque} MapSetToSet<X, Y>(xs:set<X>, f:X->Y):set<Y>

+//function MapSetToSet<X, Y>(xs:set<X>, f:X->Y):set<Y>

+  reads f.reads;

+  requires forall x :: f.requires(x);

+{

+  set x | x in xs :: f(x)

+}
\ No newline at end of file