From 6ea62e3009f326ca553521c169dec67a262a7217 Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Fri, 5 Feb 2016 18:09:23 -0800
Subject: Last checkin checked in the wrong version of bug125.dfy. The failure
 part of the test was moved into test\dafny0\modules0.dfy so that bug125.dfy
 can be verified that it was resolved to the correct types.

---
 Test/dafny4/Bug125.dfy | 24 ------------------------
 1 file changed, 24 deletions(-)

diff --git a/Test/dafny4/Bug125.dfy b/Test/dafny4/Bug125.dfy
index 916dd3f8..5dbdea6f 100644
--- a/Test/dafny4/Bug125.dfy
+++ b/Test/dafny4/Bug125.dfy
@@ -56,27 +56,3 @@ module S refines R {
    assert G.f(20); // should be LibA.G.f
   }
 } 
-
-
-module Library {
-
-  class T { }
-
-}
-
- 
-
-module A {
-
-  import opened Library
-	class T {
-	}
-}
-
- 
-
-module B refines A {
-
-  datatype T = MakeT(int)  // illegal for the same reason as above, but Dafny fails to issue an error
-
-}
-- 
cgit v1.2.3