summaryrefslogtreecommitdiff
path: root/Test/dafny4/Bug134.dfy.expect
blob: d5d7ae53947edd116f36e857a417d55309ea767b (plain)
1
2
3
4
Bug134.dfy(16,20): Warning: "import A as B" has been deprecated; in the new syntax, it is "import A:B"
Bug134.dfy(21,20): Warning: "import A as B" has been deprecated; in the new syntax, it is "import A:B"

Dafny program verifier finished with 4 verified, 0 errors