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/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index a208b1b6..d6658671 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -512,7 +512,7 @@ class AttributeTests {
 

 static method TestAttributesVarDecls()

 {

-  var {:foo} foo;

+  var {:foo} foo := null;

   var {:bar} bar := 0;

   var {:foo} {:bar} foobar : set<int> := {};

   var {:baz} baz, {:foobaz} foobaz := true, false;