From d95b2c8dd46bb52c6c84f2b764d3e6211b403346 Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Thu, 16 Apr 2015 09:50:34 -0700
Subject: Fix issue #71. When substitute the forall's variables for those of
 the fn in fixupRevealLemma substitute the types as well.

---
 Source/Dafny/DafnyAst.cs | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'Source/Dafny/DafnyAst.cs')

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 75e30b40..0b94f7fb 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -5225,12 +5225,14 @@ namespace Microsoft.Dafny {
       return e;
     }
 
-    public static Expression VarSubstituter(List<NonglobalVariable> oldVars, List<BoundVar> newVars, Expression e) {
+    public static Expression VarSubstituter(List<NonglobalVariable> oldVars, List<BoundVar> newVars, Expression e, Dictionary<TypeParameter, Type> typeMap=null) {
       Contract.Requires(oldVars != null && newVars != null);
       Contract.Requires(oldVars.Count == newVars.Count);
 
       Dictionary<IVariable, Expression/*!*/> substMap = new Dictionary<IVariable, Expression>();
-      Dictionary<TypeParameter, Type> typeMap = new Dictionary<TypeParameter, Type>();
+      if (typeMap == null) {
+        typeMap = new Dictionary<TypeParameter, Type>();
+      }
 
       for (int i = 0; i < oldVars.Count; i++) {
         var id = new IdentifierExpr(newVars[i].tok, newVars[i].Name);
-- 
cgit v1.2.3