diff options
author | leino <unknown> | 2015-05-11 01:03:03 -0700 |
---|---|---|
committer | leino <unknown> | 2015-05-11 01:03:03 -0700 |
commit | b07a96a9dca143fe669fc464dd36fee2a100d2ce (patch) | |
tree | 476d184d72c58af0271c36b998a86cf0c3431ea4 /Source | |
parent | 2e88568000690f3b5e79069e0fdcba5fef8f5ca9 (diff) |
Don't include arrow types among ordered types.
Fix bug with not seeing imap's because of type synonyms.
Don't show semi-colon after "decreases" in hover text.
Minor cosmetic change in a test case.
Diffstat (limited to 'Source')
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 2 | ||||
-rw-r--r-- | Source/Dafny/Resolver.cs | 1 |
2 files changed, 1 insertions, 2 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 83da7598..99dfecd6 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -633,7 +633,7 @@ namespace Microsoft.Dafny { /// </summary>
public bool IsOrdered {
get {
- return !IsTypeParameter && !IsCoDatatype && !(this is MapType && ((MapType)this).Finite);
+ return !IsTypeParameter && !IsCoDatatype && !IsArrowType && !IsIMapType;
}
}
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index f334fc4d..f7ec135b 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -495,7 +495,6 @@ namespace Microsoft.Dafny sep = ", ";
}
}
- s += ";"; // always terminate with a semi-colon, even in the case of an empty decreases clause
// Note, in the following line, we use the location information for "clbl", not "m". These
// are the same, except in the case where "clbl" is a CoLemma and "m" is a prefix lemma.
ReportAdditionalInformation(clbl.Tok, s, clbl.Tok.val.Length);
|