diff options
| author |  leino <unknown> | 2015-01-09 05:09:25 -0800 |
|---|---|---|
| committer | leino <unknown> | 2015-01-09 05:09:25 -0800 |
| commit | 97e7528b3cd3e9b9e21b75abf817d6e0ed3b9df7 (patch) | |
| tree | 7d94bf568cce7b5b232f32c525f05122b934054d /Test/dafny0/ResolutionErrors.dfy.expect | |
| parent | b09206df1a298d56fca3bec95baab41b7f670731 (diff) | |
When ambiguous references all resolve to the same declaration, don't complain
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy.expect')
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy.expect | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index f1c5532e..89531a5c 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -86,6 +86,7 @@ ResolutionErrors.dfy(1253,21): Error: Undeclared top-level type or type paramete ResolutionErrors.dfy(1254,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
ResolutionErrors.dfy(1291,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y)
ResolutionErrors.dfy(1301,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(1329,15): Error: The name Inner ambiguously refers to a type in one of the modules A, B
ResolutionErrors.dfy(432,2): Error: More than one anonymous constructor
ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context
ResolutionErrors.dfy(87,14): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
@@ -181,4 +182,4 @@ ResolutionErrors.dfy(1106,8): Error: new cannot be applied to a trait ResolutionErrors.dfy(1127,13): Error: first argument to / must be of numeric type (instead got set<bool>)
ResolutionErrors.dfy(1134,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating
ResolutionErrors.dfy(1149,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
-183 resolution/type errors detected in ResolutionErrors.dfy
+184 resolution/type errors detected in ResolutionErrors.dfy
|