summaryrefslogtreecommitdiff
path: root/Source/Dafny/Rewriter.cs
diff options
context:
space:
mode:
authorGravatar Dan Rosén <danr@chalmers.se>2014-08-11 16:07:38 -0700
committerGravatar Dan Rosén <danr@chalmers.se>2014-08-11 16:07:38 -0700
commit8797f054f44d114147562689d80c9970d8ea4f82 (patch)
tree6a9e99a6a39126f946c0e7dd55cf0fa03a1a0ca7 /Source/Dafny/Rewriter.cs
parent4cbe4583b329a39dee2b4b456758cafbe7e2fa79 (diff)
parent08ab990d6f1a188c6cc039d6a2289daf41ff52d3 (diff)
Merge
Diffstat (limited to 'Source/Dafny/Rewriter.cs')
-rw-r--r--Source/Dafny/Rewriter.cs6
1 files changed, 3 insertions, 3 deletions
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index f57c1380..3f4f57b8 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -174,7 +174,7 @@ namespace Microsoft.Dafny
}
} else if (member is Function && member.Name == "Valid" && !member.IsStatic) {
var fn = (Function)member;
- if (fn.Formals.Count == 0 && fn.ResultType is BoolType) {
+ if (fn.Formals.Count == 0 && fn.ResultType.IsBoolType) {
Valid = fn;
}
}
@@ -201,7 +201,7 @@ namespace Microsoft.Dafny
Boogie.IToken tok = new AutoGeneratedToken(member.tok);
if (member is Function && member.Name == "Valid" && !member.IsStatic) {
var valid = (Function)member;
- if (valid.IsGhost && valid.ResultType is BoolType) {
+ if (valid.IsGhost && valid.ResultType.IsBoolType) {
Expression c;
if (valid.RefinementBase == null) {
var c0 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.InSet, self, Repr); // this in Repr
@@ -265,7 +265,7 @@ namespace Microsoft.Dafny
var valid = new FunctionCallExpr(tok, "Valid", implicitSelf, tok, new List<Expression>());
valid.Function = Valid;
valid.Type = Type.Bool;
- // Add the identity substitution to this call
+ // Add the identity substitution to this call
valid.TypeArgumentSubstitutions = new Dictionary<TypeParameter, Type>();
foreach (var p in cl.TypeArgs) {
valid.TypeArgumentSubstitutions.Add(p, new UserDefinedType(p));