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 | |
| parent | b09206df1a298d56fca3bec95baab41b7f670731 (diff) | |
When ambiguous references all resolve to the same declaration, don't complain
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy')
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 4b290bb7..12593b8c 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -1306,3 +1306,27 @@ module FrameTargetFields { }
}
}
+
+// ------------------------------------------------------
+
+module AmbiguousModuleReference {
+ module A {
+ module Inner {
+ predicate Q()
+ }
+ }
+ module B {
+ module Inner {
+ predicate Q()
+ }
+ }
+ module OpenClient {
+ import opened A
+ import opened B
+ lemma M() {
+ var a := A.Inner.Q(); // fine
+ var b := B.Inner.Q(); // fine
+ var p := Inner.Q(); // error: Inner is ambiguous (A.Inner or B.Inner)
+ }
+ }
+}
|