6 files changed, 24 insertions, 24 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
diff --git a/Test/dafny0/CompilationErrors.dfy.expect b/Test/dafny0/CompilationErrors.dfy.expect
index e0c7f11c..e5583f30 100644
--- a/Test/dafny0/CompilationErrors.dfy.expect
+++ b/Test/dafny0/CompilationErrors.dfy.expect
@@ -1,6 +1,6 @@
 
 Dafny program verifier finished with 15 verified, 0 errors
-Compilation error: Arbitrary type ('_module.MyType') cannot be compiled
+Compilation error: Opaque type ('_module.MyType') cannot be compiled
 Compilation error: Iterator _module.Iter has no body
 Compilation error: Method _module._default.M has no body
 Compilation error: Method _module._default.P has no body
diff --git a/Test/dafny0/DisplayExpressions.dfy.expect b/Test/dafny0/DisplayExpressions.dfy.expect
index 1867ff3a..7374db2a 100644
--- a/Test/dafny0/DisplayExpressions.dfy.expect
+++ b/Test/dafny0/DisplayExpressions.dfy.expect
@@ -1,5 +1,5 @@
-DisplayExpressions.dfy(5,11): Error: the type of this map constructor is underspecified, but it cannot be an arbitrary type.
-DisplayExpressions.dfy(10,11): Error: the type of this collection constructor is underspecified, but it cannot be an arbitrary type.
-DisplayExpressions.dfy(15,11): Error: the type of this collection constructor is underspecified, but it cannot be an arbitrary type.
-DisplayExpressions.dfy(20,11): Error: the type of this collection constructor is underspecified, but it cannot be an arbitrary type.
-4 resolution/type errors detected in DisplayExpressions.dfy
+DisplayExpressions.dfy(5,11): Error: the type of this map constructor is underspecified, but it cannot be an opaque type.
+DisplayExpressions.dfy(10,11): Error: the type of this collection constructor is underspecified, but it cannot be an opaque type.
+DisplayExpressions.dfy(15,11): Error: the type of this collection constructor is underspecified, but it cannot be an opaque type.
+DisplayExpressions.dfy(20,11): Error: the type of this collection constructor is underspecified, but it cannot be an opaque type.
+4 resolution/type errors detected in DisplayExpressions.dfy
diff --git a/Test/dafny0/EqualityTypes.dfy.expect b/Test/dafny0/EqualityTypes.dfy.expect
index fde9aadf..410e4507 100644
--- a/Test/dafny0/EqualityTypes.dfy.expect
+++ b/Test/dafny0/EqualityTypes.dfy.expect
@@ -1,9 +1,9 @@
 EqualityTypes.dfy(34,13): Error: a type declaration that requires equality support cannot be replaced by a codatatype
-EqualityTypes.dfy(35,11): Error: type 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality
-EqualityTypes.dfy(40,11): Error: arbitrary type 'X' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 0)
-EqualityTypes.dfy(41,8): Error: arbitrary type 'Y' is not allowed to be replaced by a class that takes a different number of type parameters (got 1, expected 0)
-EqualityTypes.dfy(45,11): Error: type 'X' is used to refine an arbitrary type with equality support, but 'X' does not support equality
-EqualityTypes.dfy(46,11): Error: type 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality
+EqualityTypes.dfy(35,11): Error: type 'Y' is used to refine an opaque type with equality support, but 'Y' does not support equality
+EqualityTypes.dfy(40,11): Error: opaque type 'X' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 0)
+EqualityTypes.dfy(41,8): Error: opaque type 'Y' is not allowed to be replaced by a class that takes a different number of type parameters (got 1, expected 0)
+EqualityTypes.dfy(45,11): Error: type 'X' is used to refine an opaque type with equality support, but 'X' does not support equality
+EqualityTypes.dfy(46,11): Error: type 'Y' is used to refine an opaque type with equality support, but 'Y' does not support equality
 EqualityTypes.dfy(66,7): Error: == can only be applied to expressions of types that support equality (got Dt<T>)
 EqualityTypes.dfy(85,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0)
 EqualityTypes.dfy(109,7): Error: == can only be applied to expressions of types that support equality (got D)
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 38393b02..49cfe650 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -16,8 +16,8 @@ ResolutionErrors.dfy(608,10): Error: ghost variables are allowed only in specifi
 ResolutionErrors.dfy(617,17): Error: 'new' is not allowed in ghost contexts
 ResolutionErrors.dfy(619,20): Error: only ghost methods can be called from this context
 ResolutionErrors.dfy(621,8): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(639,21): Error: the type of this expression is underspecified, but it cannot be an arbitrary type.
-ResolutionErrors.dfy(639,21): Error: the type of this expression is underspecified, but it cannot be an arbitrary type.
+ResolutionErrors.dfy(639,21): Error: the type of this expression is underspecified, but it cannot be an opaque type.
+ResolutionErrors.dfy(639,21): Error: the type of this expression is underspecified, but it cannot be an opaque type.
 ResolutionErrors.dfy(676,8): Error: calls to methods with side-effects are not allowed inside a hint
 ResolutionErrors.dfy(686,8): Error: only ghost methods can be called from this context
 ResolutionErrors.dfy(689,20): Error: 'decreases *' is not allowed on ghost loops
@@ -66,7 +66,7 @@ ResolutionErrors.dfy(1007,7): Error: Cycle among type synonyms: A -> B -> A
 ResolutionErrors.dfy(1019,7): Error: Cycle among type synonyms: A -> B -> A
 ResolutionErrors.dfy(1024,7): Error: Cycle among type synonyms: A -> B -> A
 ResolutionErrors.dfy(1043,21): Error: unresolved identifier: x
-ResolutionErrors.dfy(1050,35): Error: Wrong number of type arguments (2 instead of 1) passed to arbitrary type: P
+ResolutionErrors.dfy(1050,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P
 ResolutionErrors.dfy(1062,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name?)
 ResolutionErrors.dfy(1072,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<bool>)
 ResolutionErrors.dfy(1077,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<B>)
diff --git a/Test/dafny0/TypeInstantiations.dfy.expect b/Test/dafny0/TypeInstantiations.dfy.expect
index 6c214970..30b74f8c 100644
--- a/Test/dafny0/TypeInstantiations.dfy.expect
+++ b/Test/dafny0/TypeInstantiations.dfy.expect
@@ -1,13 +1,13 @@
-TypeInstantiations.dfy(33,7): Error: an arbitrary type declaration (B) in a refining module cannot replace a more specific type declaration in the refinement base
+TypeInstantiations.dfy(33,7): Error: an opaque type declaration (B) in a refining module cannot replace a more specific type declaration in the refinement base
 TypeInstantiations.dfy(36,13): Error: a type declaration that requires equality support cannot be replaced by a codatatype
-TypeInstantiations.dfy(40,7): Error: arbitrary type 'G' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 0)
-TypeInstantiations.dfy(41,7): Error: arbitrary type 'H' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 2)
-TypeInstantiations.dfy(42,7): Error: arbitrary type 'J' is not allowed to be replaced by a type that takes a different number of type parameters (got 0, expected 1)
-TypeInstantiations.dfy(51,8): Error: arbitrary type 'R' is not allowed to be replaced by a type that takes a different number of type parameters (got 0, expected 1)
-TypeInstantiations.dfy(53,8): Error: arbitrary type 'T' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 0)
+TypeInstantiations.dfy(40,7): Error: opaque type 'G' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 0)
+TypeInstantiations.dfy(41,7): Error: opaque type 'H' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 2)
+TypeInstantiations.dfy(42,7): Error: opaque type 'J' is not allowed to be replaced by a type that takes a different number of type parameters (got 0, expected 1)
+TypeInstantiations.dfy(51,8): Error: opaque type 'R' is not allowed to be replaced by a type that takes a different number of type parameters (got 0, expected 1)
+TypeInstantiations.dfy(53,8): Error: opaque type 'T' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 0)
 TypeInstantiations.dfy(55,7): Error: type 'TP0' is not allowed to change its number of type parameters (got 1, expected 0)
 TypeInstantiations.dfy(56,7): Error: type 'TP1' is not allowed to change its number of type parameters (got 0, expected 1)
-TypeInstantiations.dfy(34,11): Error: type 'C' is used to refine an arbitrary type with equality support, but 'C' does not support equality
-TypeInstantiations.dfy(35,7): Error: type 'D' is used to refine an arbitrary type with equality support, but 'D' does not support equality
-TypeInstantiations.dfy(48,7): Error: type 'N' is used to refine an arbitrary type with equality support, but 'N' does not support equality
+TypeInstantiations.dfy(34,11): Error: type 'C' is used to refine an opaque type with equality support, but 'C' does not support equality
+TypeInstantiations.dfy(35,7): Error: type 'D' is used to refine an opaque type with equality support, but 'D' does not support equality
+TypeInstantiations.dfy(48,7): Error: type 'N' is used to refine an opaque type with equality support, but 'N' does not support equality
 12 resolution/type errors detected in TypeInstantiations.dfy