diff options
| author |  leino <unknown> | 2014-10-28 17:44:39 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-10-28 17:44:39 -0700 |
| commit | 655b8311917e38cc2b359bad46def21de7852508 (patch) | |
| tree | 8c7881bac939013d25a28e82e9860c456f034ea0 /Test/dafny0/ResolutionErrors.dfy.expect | |
| parent | 6c9a50e81dbdb791c558ac0a3463f01ee6a7f580 (diff) | |
Disallow automatic completion of type arguments to the LHS of datatype declarations
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy.expect')
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy.expect | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 1b802687..3b768c84 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -83,6 +83,8 @@ ResolutionErrors.dfy(1220,26): Error: the type of this variable is underspecifie ResolutionErrors.dfy(1221,31): Error: the type of this variable is underspecified
ResolutionErrors.dfy(1222,29): Error: the type of this variable is underspecified
ResolutionErrors.dfy(1232,34): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1248,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
+ResolutionErrors.dfy(1249,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
ResolutionErrors.dfy(429,2): Error: More than one anonymous constructor
ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context
ResolutionErrors.dfy(111,9): Error: ghost variables are allowed only in specification contexts
@@ -180,4 +182,4 @@ ResolutionErrors.dfy(1101,8): Error: new cannot be applied to a trait ResolutionErrors.dfy(1122,13): Error: first argument to / must be of numeric type (instead got set<bool>)
ResolutionErrors.dfy(1129,2): 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(1144,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
-182 resolution/type errors detected in ResolutionErrors.dfy
+184 resolution/type errors detected in ResolutionErrors.dfy
|