Dafny:

* started rewriting parsing of qualified identifiers in expressions
* annoyingly, had to introduce AST nodes for concrete syntax
* previous syntax for invoking datatype constructors: #List.Cons(h, t)
  new syntax:  List.Cons(h, t)
  or, if only one datatype has a constructor named Cons:  Cons(h, t)
* Removed type parameters for datatype constructors from the grammar
* Helped Test/VSI-Benchmarks/b4.dfy along with a couple of assertions (previously, its proving performance was highly varied)

1 files changed, 2 insertions, 2 deletions

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 792c8fac..7deeb0a1 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -1,9 +1,9 @@
 class C {

   function F(c: C, d: D): bool { true }

   method M(x: int) returns (y: int, c: C)

-    requires F(#D.A, this);  // 2 errors

+    requires F(D.A, this);  // 2 errors

     requires F(4, 5);  // 2 errors

-    requires F(this, #D.A);  // good

+    requires F(this, D.A);  // good

   { }

 

   method Caller()