clarified error message that occurs when the "opened" keyword is left off of a module import.

5 files changed, 19 insertions, 19 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 8d23f374..26349ef5 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -8593,7 +8593,7 @@ namespace Microsoft.Dafny
 #endif

       } else {

         // ----- None of the above

-        Error(expr.tok, "Undeclared top-level type or type parameter: {0} (did you forget to qualify a name?)", expr.Name);

+        Error(expr.tok, "Undeclared top-level type or type parameter: {0} (did you forget to qualify a name or declare a module import 'opened?')", expr.Name);

       }

 

       if (r == null) {

diff --git a/Test/dafny0/Modules0.dfy.expect b/Test/dafny0/Modules0.dfy.expect
index d2f0bcc8..c63ed937 100644
--- a/Test/dafny0/Modules0.dfy.expect
+++ b/Test/dafny0/Modules0.dfy.expect
@@ -6,17 +6,17 @@ Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupA
 Modules0.dfy(13,7): Error: Duplicate name of top-level declaration: WazzupB

 Modules0.dfy(14,8): Error: Duplicate name of top-level declaration: WazzupB

 Modules0.dfy(15,11): Error: Duplicate name of top-level declaration: WazzupB

-Modules0.dfy(56,21): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget to qualify a name?)

-Modules0.dfy(57,21): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)

-Modules0.dfy(68,21): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)

-Modules0.dfy(84,24): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?)

-Modules0.dfy(93,19): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?)

-Modules0.dfy(226,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)

+Modules0.dfy(56,21): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget to qualify a name or declare a module import 'opened?')

+Modules0.dfy(57,21): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name or declare a module import 'opened?')

+Modules0.dfy(68,21): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name or declare a module import 'opened?')

+Modules0.dfy(84,24): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name or declare a module import 'opened?')

+Modules0.dfy(93,19): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name or declare a module import 'opened?')

+Modules0.dfy(226,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')

 Modules0.dfy(226,8): Error: new can be applied only to reference types (got X)

 Modules0.dfy(235,13): Error: module 'B' does not declare a type 'X'

 Modules0.dfy(245,13): Error: unresolved identifier: X

 Modules0.dfy(246,15): Error: member DoesNotExist does not exist in class X

-Modules0.dfy(285,19): Error: Undeclared top-level type or type parameter: D (did you forget to qualify a name?)

+Modules0.dfy(285,19): Error: Undeclared top-level type or type parameter: D (did you forget to qualify a name or declare a module import 'opened?')

 Modules0.dfy(285,12): Error: new can be applied only to reference types (got D)

 Modules0.dfy(288,25): Error: type of the receiver is not fully determined at this program point

 Modules0.dfy(289,16): Error: type of the receiver is not fully determined at this program point

@@ -25,10 +25,10 @@ Modules0.dfy(290,16): Error: type of the receiver is not fully determined at thi
 Modules0.dfy(290,17): Error: expected method call, found expression

 Modules0.dfy(314,18): Error: second argument to "in" must be a set, multiset, or sequence with elements of type Q_Imp.Node, or a map with domain Q_Imp.Node (instead got set<Node>)

 Modules0.dfy(318,13): Error: arguments must have the same type (got Q_Imp.Node and Node)

-Modules0.dfy(319,11): Error: Undeclared top-level type or type parameter: LongLostModule (did you forget to qualify a name?)

-Modules0.dfy(320,11): Error: Undeclared top-level type or type parameter: Wazzup (did you forget to qualify a name?)

+Modules0.dfy(319,11): Error: Undeclared top-level type or type parameter: LongLostModule (did you forget to qualify a name or declare a module import 'opened?')

+Modules0.dfy(320,11): Error: Undeclared top-level type or type parameter: Wazzup (did you forget to qualify a name or declare a module import 'opened?')

 Modules0.dfy(321,17): Error: module 'Q_Imp' does not declare a type 'Edon'

 Modules0.dfy(323,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)

 Modules0.dfy(324,30): Error: member Create does not exist in class Klassy

-Modules0.dfy(101,14): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?)

+Modules0.dfy(101,14): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name or declare a module import 'opened?')

 31 resolution/type errors detected in Modules0.dfy

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index c215d354..ae3e8cbf 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -58,8 +58,8 @@ ResolutionErrors.dfy(987,11): Error: Wrong number of type arguments (2 instead o
 ResolutionErrors.dfy(988,11): Error: Wrong number of type arguments (2 instead of 1) passed to class: C

 ResolutionErrors.dfy(999,7): Error: Duplicate name of top-level declaration: BadSyn2

 ResolutionErrors.dfy(996,17): Error: Wrong number of type arguments (0 instead of 1) passed to datatype: List

-ResolutionErrors.dfy(997,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name?)

-ResolutionErrors.dfy(998,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)

+ResolutionErrors.dfy(997,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name or declare a module import 'opened?')

+ResolutionErrors.dfy(998,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')

 ResolutionErrors.dfy(1005,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> A

 ResolutionErrors.dfy(1008,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A

 ResolutionErrors.dfy(1012,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A

@@ -68,7 +68,7 @@ ResolutionErrors.dfy(1024,7): Error: Cycle among redirecting types (newtypes, ty
 ResolutionErrors.dfy(1029,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A

 ResolutionErrors.dfy(1048,21): Error: unresolved identifier: x

 ResolutionErrors.dfy(1055,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P

-ResolutionErrors.dfy(1067,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name?)

+ResolutionErrors.dfy(1067,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name or declare a module import 'opened?')

 ResolutionErrors.dfy(1077,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<bool>)

 ResolutionErrors.dfy(1082,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<B>)

 ResolutionErrors.dfy(1087,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<int>)

@@ -82,8 +82,8 @@ ResolutionErrors.dfy(1225,26): Error: the type of this variable is underspecifie
 ResolutionErrors.dfy(1226,31): Error: the type of this variable is underspecified

 ResolutionErrors.dfy(1227,29): Error: the type of this variable is underspecified

 ResolutionErrors.dfy(1237,34): Error: the type of this variable is underspecified

-ResolutionErrors.dfy(1253,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)

-ResolutionErrors.dfy(1254,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)

+ResolutionErrors.dfy(1253,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')

+ResolutionErrors.dfy(1254,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')

 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 (try qualifying the type name with the module name)

diff --git a/Test/dafny0/Trait/TraitBasix.dfy.expect b/Test/dafny0/Trait/TraitBasix.dfy.expect
index 69af0dc5..dbb11c21 100644
--- a/Test/dafny0/Trait/TraitBasix.dfy.expect
+++ b/Test/dafny0/Trait/TraitBasix.dfy.expect
@@ -1,4 +1,4 @@
-TraitBasix.dfy(91,24): Error: Undeclared top-level type or type parameter: IX (did you forget to qualify a name?)

+TraitBasix.dfy(91,24): Error: Undeclared top-level type or type parameter: IX (did you forget to qualify a name or declare a module import 'opened?')

 TraitBasix.dfy(77,8): Error: field 'x' is inherited from trait 'I2' and is not allowed to be re-declared

 TraitBasix.dfy(70,8): Error: class 'I0Child' does not implement trait method 'I2.Customizable'

 TraitBasix.dfy(80,8): Error: class 'I0Child2' does not implement trait function 'I2.F'

diff --git a/Test/dafny0/UserSpecifiedTypeParameters.dfy.expect b/Test/dafny0/UserSpecifiedTypeParameters.dfy.expect
index 2504fbfb..347252aa 100644
--- a/Test/dafny0/UserSpecifiedTypeParameters.dfy.expect
+++ b/Test/dafny0/UserSpecifiedTypeParameters.dfy.expect
@@ -1,8 +1,8 @@
 UserSpecifiedTypeParameters.dfy(27,12): Error: the type of this variable is underspecified

 UserSpecifiedTypeParameters.dfy(27,26): Error: type variable 'T' in the function call to 'H' could not be determined

 UserSpecifiedTypeParameters.dfy(27,26): Error: type variable 'U' in the function call to 'H' could not be determined

-UserSpecifiedTypeParameters.dfy(48,22): Error: Undeclared top-level type or type parameter: b (did you forget to qualify a name?)

-UserSpecifiedTypeParameters.dfy(48,26): Error: Undeclared top-level type or type parameter: c (did you forget to qualify a name?)

+UserSpecifiedTypeParameters.dfy(48,22): Error: Undeclared top-level type or type parameter: b (did you forget to qualify a name or declare a module import 'opened?')

+UserSpecifiedTypeParameters.dfy(48,26): Error: Undeclared top-level type or type parameter: c (did you forget to qualify a name or declare a module import 'opened?')

 UserSpecifiedTypeParameters.dfy(48,18): Error: variable 'a' does not take any type parameters

 UserSpecifiedTypeParameters.dfy(48,30): Error: non-function expression (of type int) is called with parameters

 UserSpecifiedTypeParameters.dfy(48,16): Error: wrong number of arguments to function application (function 'F' expects 2, got 1)