summaryrefslogtreecommitdiff
path: root/Test/dafny3/Zip.dfy
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny3/Zip.dfy')
-rw-r--r--Test/dafny3/Zip.dfy2
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny3/Zip.dfy b/Test/dafny3/Zip.dfy
index 371b012a..80e8cd91 100644
--- a/Test/dafny3/Zip.dfy
+++ b/Test/dafny3/Zip.dfy
@@ -8,7 +8,7 @@ properties, drawing from:
Some proofs are automatic (EvenZipLemma), whereas some others require a single
recursive call to be made explicitly.
-Note that the automatically inserted parallel statement
+Note that the automatically inserted forall statement
is in principle strong enough in all cases above, but the incompletness
of reasoning with quantifiers in SMT solvers make the explicit calls
necessary.