Dafny: retired the "call" keyword

1 files changed, 4 insertions, 4 deletions

diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy
index 161ac22f..e4d0cbe7 100644
--- a/Test/dafny0/NatTypes.dfy
+++ b/Test/dafny0/NatTypes.dfy
@@ -3,8 +3,8 @@ method M(n: nat) {
 }

 

 method Main() {

-  call M(25);

-  call M(-25);  // error: cannot pass -25 as a nat

+  M(25);

+  M(-25);  // error: cannot pass -25 as a nat

 }

 

 var f: nat;

@@ -34,7 +34,7 @@ method CheckField(x: nat, y: int)
 method Generic<T>(i: int, t0: T, t1: T) returns (r: T) {

   if (0 < i) {

     var n: nat := 5;

-    call j := Generic(i-1, n, -4);

+    var j := Generic(i-1, n, -4);

     assert 0 <= j;  // error: the result is an int, not a nat

     var q := FenEric(n, -4);

     assert 0 <= q;  // error: the result is an int, not a nat

@@ -65,7 +65,7 @@ method MatchIt(list: List<object>) returns (k: nat)
   match (list) {

     case Nil =>

     case Cons(n, extra, tail) =>

-      call w := MatchIt(tail);

+      var w := MatchIt(tail);

       assert 0 <= w;

       assert 0 <= n;  // fine

       assert 0 <= n - 10;  // error: possible assertion failure