diff options
| author |  leino <unknown> | 2015-08-11 19:12:43 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-08-11 19:12:43 -0700 |
| commit | 34cb773ec61c32479c8d189b23e000af956cc28e (patch) | |
| tree | 63bf936a722fa73cbdf1480a69bbca0a308ccd07 /Source/Dafny/Rewriter.cs | |
| parent | 3bf4b44b821dca5017017e99502f263e636d5e84 (diff) | |
Removed the unused type ThisSurrogate
Diffstat (limited to 'Source/Dafny/Rewriter.cs')
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index ffd808c5..7ab7dd36 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -1475,9 +1475,7 @@ namespace Microsoft.Dafny // The following variable is what gets passed down to recursive calls if the subexpression does not itself acquire prominent status.
var subExprIsProminent = DafnyOptions.O.InductionHeuristic == 2 || DafnyOptions.O.InductionHeuristic == 4 ? /*once prominent, always prominent*/exprIsProminent : /*reset the prominent status*/false;
- if (expr is ThisExpr) {
- return exprIsProminent && n is ThisSurrogate;
- } else if (expr is IdentifierExpr) {
+ if (expr is IdentifierExpr) {
var e = (IdentifierExpr)expr;
return exprIsProminent && e.Var == n;
} else if (expr is SeqSelectExpr) {
|