diff options
| author |  Rustan Leino <unknown> | 2015-08-20 17:29:15 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2015-08-20 17:29:15 -0700 |
| commit | efcd1e908cb7ea05e78faffd206fa5ce1e966b74 (patch) | |
| tree | 7b6ff26639813f2a059f427aab7dc00fccd924f0 /Source/Dafny/Resolver.cs | |
| parent | b8d7d6d785a29fd948e9a9740fb96ed270ac19d8 (diff) | |
Changed equality tests involving traits from using strings to using reference equality
Diffstat (limited to 'Source/Dafny/Resolver.cs')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 2f2b5a54..a1e89805 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -4342,13 +4342,12 @@ namespace Microsoft.Dafny successSoFar = UnifyTypes(aa.TypeArgs[i], bb.TypeArgs[i]);
}
return successSoFar;
- }
- else if ((rcb is TraitDecl) && (rca is TraitDecl)) {
- return ((TraitDecl)rcb).FullCompileName == ((TraitDecl)rca).FullCompileName;
- } else if ((rcb is ClassDecl) && (rca is TraitDecl)) {
- return ((ClassDecl)rcb).TraitsObj.Any(tr => tr.FullCompileName == ((TraitDecl)rca).FullCompileName);
- } else if ((rca is ClassDecl) && (rcb is TraitDecl)) {
- return ((ClassDecl)rca).TraitsObj.Any(tr => tr.FullCompileName == ((TraitDecl)rcb).FullCompileName);
+ } else if (rcb is TraitDecl && rca is TraitDecl) {
+ return rca == rcb;
+ } else if (rcb is ClassDecl && rca is TraitDecl) {
+ return ((ClassDecl)rcb).TraitsObj.Contains(rca);
+ } else if (rca is ClassDecl && rcb is TraitDecl) {
+ return ((ClassDecl)rca).TraitsObj.Contains(rcb);
} else if (aa.ResolvedParam != null && aa.ResolvedParam == bb.ResolvedParam) {
// type parameters
if (aa.TypeArgs.Count != bb.TypeArgs.Count) {
|