summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar chrishaw <unknown>2015-03-17 12:57:58 -0700
committerGravatar chrishaw <unknown>2015-03-17 12:57:58 -0700
commitf3aec1ea3cd22edf386b8ded4d705d2c41b1ecc7 (patch)
tree6104f2287dbc37a97640de0c4209f4d94533f137 /Source
parentfef0fb324b51c0113871bb78b91f2c8c516e9b2b (diff)
parent2184631376ff382b8b63908929b16ddd97afdc90 (diff)
Merge
Diffstat (limited to 'Source')
-rw-r--r--Source/Dafny/Translator.cs4
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index a150eecd..f3572948 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -13418,9 +13418,9 @@ namespace Microsoft.Dafny {
newExpr = new NamedExpr(e.tok, e.Name, body, contract, e.ReplacerToken);
} else if (expr is ComprehensionExpr) {
var e = (ComprehensionExpr)expr;
- // For quantifiers we want to make sure that we don't introduce name clashes with
+ // For quantifiers and setComprehesion we want to make sure that we don't introduce name clashes with
// the enclosing scopes.
- var newBoundVars = CreateBoundVarSubstitutions(e.BoundVars, expr is ForallExpr || expr is ExistsExpr);
+ var newBoundVars = CreateBoundVarSubstitutions(e.BoundVars, expr is ForallExpr || expr is ExistsExpr || expr is SetComprehension);
Expression newRange = e.Range == null ? null : Substitute(e.Range);
Expression newTerm = Substitute(e.Term);
Attributes newAttrs = SubstAttributes(e.Attributes);