diff options
| author |  leino <unknown> | 2015-04-05 01:56:49 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-04-05 01:56:49 -0700 |
| commit | e9c7c508c1900e6195164d263c9249e3c7b56b51 (patch) | |
| tree | 015bbdd42d118838ed4d2a758444d7e1eb55d46b /Test/dafny0/Trait/TraitMultiModule.dfy.expect | |
| parent | cee337934c619bfeb646d83243eff1f08e83902d (diff) | |
Fixed some bugs in override axioms (but still missing support for classes with type parameters).
Resolve ClassDecl.TraitsTyp as types.
Moved declaration of TraitParent and NoTraitAtAll to prelude.
Diffstat (limited to 'Test/dafny0/Trait/TraitMultiModule.dfy.expect')
| -rw-r--r-- | Test/dafny0/Trait/TraitMultiModule.dfy.expect | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/Test/dafny0/Trait/TraitMultiModule.dfy.expect b/Test/dafny0/Trait/TraitMultiModule.dfy.expect index a1617395..e991553a 100644 --- a/Test/dafny0/Trait/TraitMultiModule.dfy.expect +++ b/Test/dafny0/Trait/TraitMultiModule.dfy.expect @@ -1,2 +1,3 @@ -TraitMultiModule.dfy(21,19): Error: class M2.C2 is in a different module than trait M1.T1. A class may only extend a trait in the same module
-1 resolution/type errors detected in TraitMultiModule.dfy
+TraitMultiModule.dfy(22,19): Error: class 'C2' is in a different module than trait 'M1.T1'. A class may only extend a trait in the same module.
+TraitMultiModule.dfy(30,22): Error: class 'C2' is in a different module than trait 'M1.T1'. A class may only extend a trait in the same module.
+2 resolution/type errors detected in TraitMultiModule.dfy
|