Fixed bug #33.

3 files changed, 21 insertions, 1 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 3532c8e6..d2fc74aa 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1106,6 +1106,9 @@ namespace Microsoft.Dafny
         return new UserDefinedType(tt.tok, tt.Name, tt.TypeArgs.ConvertAll(CloneType), tt.Path.ConvertAll(x => x));

       } else if (t is InferredTypeProxy) {

         return new InferredTypeProxy();

+      } else if (t is ParamTypeProxy) {

+        var tt = (ParamTypeProxy)t;

+        return new ParamTypeProxy(CloneTypeParam(tt.orig));

       } else {

         Contract.Assert(false);  // unexpected type (e.g., no other type proxies are expected at this time)

         return null;  // to please compiler

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 57c0b11e..34c51d58 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -792,7 +792,7 @@ Modules1.dfy(59,3): Error: failure to decrease termination measure
 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 22 verified, 5 errors

+Dafny program verifier finished with 26 verified, 5 errors

 

 -------------------- Modules2.dfy --------------------

 Modules2.dfy(44,17): Error: The name C ambiguously refers to a type in one of the modules A, B (try qualifying the type name with the module name)

diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy
index e9c432f3..3f24212b 100644
--- a/Test/dafny0/Modules1.dfy
+++ b/Test/dafny0/Modules1.dfy
@@ -113,3 +113,20 @@ module Q_M {
     var q := new Q.Klassy.Init();

   }

 }

+

+// ----- regression test -----------------------------------------

+

+abstract module Regression {

+  module A

+  {

+    predicate p(m: map)

+

+    lemma m(m: map)

+      ensures exists m :: p(m);

+  }

+

+  abstract module B

+  {

+    import X as A

+  }

+}