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/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy
index 0d69b1b8..33442219 100644
--- a/Test/dafny1/SchorrWaite.dfy
+++ b/Test/dafny1/SchorrWaite.dfy
@@ -182,7 +182,7 @@ class Main {
   {

     var t := root;

     var p: Node := null;  // parent of t in original graph

-    ghost var path := #Path.Empty;

+    ghost var path := Path.Empty;

     t.marked := true;

     t.pathFromRoot := path;

     ghost var stackNodes := [];

@@ -256,7 +256,7 @@ class Main {
         t.children := t.children[..t.childrenVisited] + [p] + t.children[t.childrenVisited + 1..];

         p := t;

         stackNodes := stackNodes + [t];

-        path := #Path.Extend(path, t);

+        path := Path.Extend(path, t);

         t := newT;

         t.marked := true;

         t.pathFromRoot := path;