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, 1 insertions, 1 deletions

diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy
index 6b7ce9b9..161ac22f 100644
--- a/Test/dafny0/NatTypes.dfy
+++ b/Test/dafny0/NatTypes.dfy
@@ -47,7 +47,7 @@ function method FenEric<T>(t0: T, t1: T): T;
 datatype Pair<T> { Pr(T, T); }

 

 method K(n: nat, i: int) {

-  match (#Pair.Pr(n, i)) {

+  match (Pair.Pr(n, i)) {

     case Pr(k, l) =>

       assert k == n;  // fine: although the type of k is int, we know it's equal to n

       assert 0 <= k;