diff options
| author |  Rustan Leino <unknown> | 2013-12-20 11:11:05 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-12-20 11:11:05 -0800 |
| commit | 1d2ae01b786addc664f34e719421c81037ae0fe0 (patch) | |
| tree | 31f331f8ccea5a4507c644f41a454cd5f14f8ca4 /Source/Dafny/RefinementTransformer.cs | |
| parent | 14b738e4e40215ddb2442f2294caf7734e9bed07 (diff) | |
Changed the iterator class hover text back to the iterator name (which is consistent with everything else), not the "iterator" keyword
Diffstat (limited to 'Source/Dafny/RefinementTransformer.cs')
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index c410d56d..3b04e017 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -608,8 +608,8 @@ namespace Microsoft.Dafny var yens = prev.YieldEnsures.ConvertAll(rawCloner.CloneMayBeFreeExpr);
yens.AddRange(nw.YieldEnsures);
- return new IteratorDecl(new RefinementToken(nw.IteratorKeywordTok, moduleUnderConstruction),
- new RefinementToken(nw.tok, moduleUnderConstruction), nw.Name, moduleUnderConstruction,
+ return new IteratorDecl(new RefinementToken(nw.tok, moduleUnderConstruction),
+ nw.Name, moduleUnderConstruction,
nw.SignatureIsOmitted ? prev.TypeArgs.ConvertAll(refinementCloner.CloneTypeParam) : nw.TypeArgs,
nw.SignatureIsOmitted ? prev.Ins.ConvertAll(refinementCloner.CloneFormal) : nw.Ins,
nw.SignatureIsOmitted ? prev.Outs.ConvertAll(refinementCloner.CloneFormal) : nw.Outs,
|