Stricter rules about that types need to be completely resolved.

Renamed "default constructor" to "anonymous constructor" (since there's really nothing "default" about it).
If the type of literal "null" is unresolved, make the type "object".
The need to translate unresolved proxies is now assumed to be gone.

1 files changed, 1 insertions, 1 deletions

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 31819dcc..6086fcf1 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -68,7 +68,7 @@ method DuplicateVarName(x: int) returns (y: int)
 method ScopeTests()

 {

   var x := x;  // error: the 'x' in the RHS is not in scope

-  var y :| y == y;  // fine, 'y' is in scope in the RHS

+  var y: real :| y == y;  // fine, 'y' is in scope in the RHS

   var z := DuplicateVarName(z);  // error: the 'z' in the RHS is not in scope

   var w0, w1 := IntTransform(w1), IntTransform(w0);  // errors two

   var c := new MyClass.Init(null);  // fine