diff options
| author |  Rustan Leino <unknown> | 2014-07-15 17:16:02 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-07-15 17:16:02 -0700 |
| commit | 17bd465d7950927d76080106db7ade928e5a8b4a (patch) | |
| tree | 6cd72cca845197ea03536cce91a2f66cb1e88998 /Test/dafny0/TypeInstantiations.dfy.expect | |
| parent | 30cd666db7142297b7cd627cad34243b76e7291a (diff) | |
Renamed "arbitrary type" to "opaque type"
Diffstat (limited to 'Test/dafny0/TypeInstantiations.dfy.expect')
| -rw-r--r-- | Test/dafny0/TypeInstantiations.dfy.expect | 18 |
1 files changed, 9 insertions, 9 deletions
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
|