summaryrefslogtreecommitdiff
path: root/Test/dafny0/Trait
diff options
context:
space:
mode:
authorGravatar Michael Lowell Roberts <mirobert@microsoft.com>2015-07-20 14:06:06 -0700
committerGravatar Michael Lowell Roberts <mirobert@microsoft.com>2015-07-20 14:06:06 -0700
commit701741248e5831c1976b8cb2a2cc412987a1332e (patch)
tree65fe57a2b6fce3fbdde5512975bd03f09cb47618 /Test/dafny0/Trait
parent4dd4262daa0247cd78eef104ddf6083d90ee8972 (diff)
clarified error message that occurs when the "opened" keyword is left off of a module import.
Diffstat (limited to 'Test/dafny0/Trait')
-rw-r--r--Test/dafny0/Trait/TraitBasix.dfy.expect2
1 files changed, 1 insertions, 1 deletions
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'