summaryrefslogtreecommitdiff
path: root/Test/dafny0/CompilationErrors.dfy
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2014-07-15 17:16:02 -0700
committerGravatar Rustan Leino <unknown>2014-07-15 17:16:02 -0700
commit17bd465d7950927d76080106db7ade928e5a8b4a (patch)
tree6cd72cca845197ea03536cce91a2f66cb1e88998 /Test/dafny0/CompilationErrors.dfy
parent30cd666db7142297b7cd627cad34243b76e7291a (diff)
Renamed "arbitrary type" to "opaque type"
Diffstat (limited to 'Test/dafny0/CompilationErrors.dfy')
-rw-r--r--Test/dafny0/CompilationErrors.dfy2
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny0/CompilationErrors.dfy b/Test/dafny0/CompilationErrors.dfy
index 2f3325a1..80e5eeae 100644
--- a/Test/dafny0/CompilationErrors.dfy
+++ b/Test/dafny0/CompilationErrors.dfy
@@ -1,7 +1,7 @@
// RUN: %dafny "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
-type MyType // compile error: arbitrary type
+type MyType // compile error: opaque type
iterator Iter() // compile error: body-less iterator
ghost method M() // compile error: body-less ghost method
method P() // compile error: body-less method