diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-21 19:24:31 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-21 19:24:31 -0700 |
| commit | e33ab2dea7b3a367d2bb5c0d3926fa6fcc790ed4 (patch) | |
| tree | 25c5aba0d4aef70b6334de449c5921f38561806f /Source/Dafny/Resolver.cs | |
| parent | ff05bb6936d433e7be5ded41233214c0517dc2d2 (diff) | |
| parent | 2befeb58569d39056e3d0797c901293446a14d03 (diff) | |
Merge
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 e5fe7cf8..899d0a3d 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) {
|