diff options
| author |  Rustan Leino <leino@microsoft.com> | 2013-06-25 19:10:46 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2013-06-25 19:10:46 -0700 |
| commit | bee0b2048bdfe1d93815819619aa322ecb5fbf97 (patch) | |
| tree | 63448281f4dd2854d4a5b7a43e4bc3f7a541b31f /Source/Dafny/Resolver.cs | |
| parent | b443322c8ce89ac68f0aa7cca49cd406cade7641 (diff) | |
Fixed some Code Contract type errors
Diffstat (limited to 'Source/Dafny/Resolver.cs')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 46c0808d..d6393b02 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -6455,11 +6455,11 @@ namespace Microsoft.Dafny Contract.Ensures(
(returnAllBounds && Contract.OldValue(missingBounds.Count) <= missingBounds.Count) ||
(!returnAllBounds &&
- Contract.Result<List<ComprehensionExpr.BoundedPool>>() != null &&
- Contract.Result<List<ComprehensionExpr.BoundedPool>>().Count == bvars.Count &&
+ Contract.Result<List<Tuple<VT, List<ComprehensionExpr.BoundedPool>>>>() != null &&
+ Contract.Result<List<Tuple<VT, List<ComprehensionExpr.BoundedPool>>>>().Count == bvars.Count &&
Contract.OldValue(missingBounds.Count) == missingBounds.Count) ||
(!returnAllBounds &&
- Contract.Result<List<ComprehensionExpr.BoundedPool>>() == null &&
+ Contract.Result<List<Tuple<VT, List<ComprehensionExpr.BoundedPool>>>>() == null &&
Contract.OldValue(missingBounds.Count) < missingBounds.Count));
var allBounds = new List<Tuple<VT, List<ComprehensionExpr.BoundedPool>>>();
|