Fix atg file and add comment about Set/*Variable*/

2 files changed, 2 insertions, 2 deletions

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 7e5651f2..86fda429 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -18,7 +18,7 @@ namespace Microsoft.Boogie {
   using System.Diagnostics.Contracts;

   using Microsoft.Basetypes;

 

-  using Set = GSet<object>;

+  using Set = GSet<object>; // not that the set used is not a set of Variable only, as it also contains TypeVariables

 

 

   //---------------------------------------------------------------------

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index c7950c9a..33172e7f 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -97,7 +97,7 @@ private class BvBounds : Expr {
     Contract.Requires(stream != null);

     {Contract.Assert(false);throw new cce.UnreachableException();}

   }

-  public override void ComputeFreeVariables(Set/*!*/ freeVars) {Contract.Requires(freeVars != null); {Contract.Assert(false);throw new cce.UnreachableException();} }

+  public override void ComputeFreeVariables(GSet<object>/*!*/ freeVars) {Contract.Requires(freeVars != null); {Contract.Assert(false);throw new cce.UnreachableException();} }

   public override AI.IExpr/*!*/ IExpr { get { Contract.Ensures(Contract.Result<AI.IExpr>()!=null); {Contract.Assert(false);throw new cce.UnreachableException();} } }

 }