From 5049ea124fe4b34f5c8fcb244663f3b68053643e Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Fri, 3 Jan 2014 18:16:07 -0800
Subject: Renamed a constructor in a test file

---
 Test/dafny2/TreeFill.dfy | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'Test/dafny2')

diff --git a/Test/dafny2/TreeFill.dfy b/Test/dafny2/TreeFill.dfy
index f7e2cc89..3328aca9 100644
--- a/Test/dafny2/TreeFill.dfy
+++ b/Test/dafny2/TreeFill.dfy
@@ -1,9 +1,9 @@
-datatype Tree<T> = Null | Node(Tree, T, Tree);
+datatype Tree<T> = Leaf | Node(Tree, T, Tree)
 
 function Contains<T>(t: Tree, v: T): bool
 {
   match t
-  case Null => false
+  case Leaf => false
   case Node(left, x, right) => x == v || Contains(left, v) || Contains(right, v)
 }
 
@@ -14,12 +14,12 @@ method Fill<T>(t: Tree, a: array<T>, start: int) returns (end: int)
   ensures forall i :: 0 <= i < start ==> a[i] == old(a[i]);
   ensures forall i :: start <= i < end ==> Contains(t, a[i]);
 {
-  match (t) {
-    case Null =>
+  match t {
+    case Leaf =>
       end := start;
     case Node(left, x, right) =>
       end := Fill(left, a, start);
-      if (end < a.Length) {
+      if end < a.Length {
         a[end] := x;
         end := Fill(right, a, end + 1);
       }
-- 
cgit v1.2.3