diff options
author | Jason Koenig <unknown> | 2011-07-15 18:08:08 -0700 |
---|---|---|
committer | Jason Koenig <unknown> | 2011-07-15 18:08:08 -0700 |
commit | b32e450d37de5797eb143dce80866e863d498102 (patch) | |
tree | 877bded3befc7db1599061dcced086d464c73242 /Source/Dafny/DafnyAst.cs | |
parent | 1f850973d1c80f9474a9b07571c35d37a1a25368 (diff) | |
parent | fb0960efe49ccb771ffee57e2cfaccdac6db4e04 (diff) |
Merge
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 871a8b34..218f95e5 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -413,13 +413,13 @@ namespace Microsoft.Dafny { /// <summary>
/// This proxy stands for any type.
- /// </summary>
+ /// </summary>
public class InferredTypeProxy : UnrestrictedTypeProxy {
}
/// <summary>
/// This proxy stands for any type, but it originates from an instantiated type parameter.
- /// </summary>
+ /// </summary>
public class ParamTypeProxy : UnrestrictedTypeProxy {
TypeParameter orig;
[ContractInvariantMethod]
@@ -445,7 +445,7 @@ namespace Microsoft.Dafny { /// <summary>
/// This proxy stands for any datatype.
- /// </summary>
+ /// </summary>
public class DatatypeProxy : RestrictedTypeProxy {
public override int OrderID {
get {
@@ -456,7 +456,7 @@ namespace Microsoft.Dafny { /// <summary>
/// This proxy stands for object or any class/array type.
- /// </summary>
+ /// </summary>
public class ObjectTypeProxy : RestrictedTypeProxy {
public override int OrderID {
get {
@@ -504,7 +504,7 @@ namespace Microsoft.Dafny { /// if AllowSeq, or:
/// int or set or multiset
/// if !AllowSeq.
- /// </summary>
+ /// </summary>
public class OperationTypeProxy : RestrictedTypeProxy {
public readonly bool AllowSeq;
public OperationTypeProxy(bool allowSeq) {
@@ -688,7 +688,7 @@ namespace Microsoft.Dafny { public class ClassRefinementDecl : ClassDecl {
public readonly IToken/*!*/ RefinedClass;
- public ClassDecl Refined; // filled in during resolution
+ public ClassDecl Refined; // filled in during resolution
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(RefinedClass != null);
@@ -733,7 +733,7 @@ namespace Microsoft.Dafny { Dims = dims;
}
}
-
+
public class DatatypeDecl : TopLevelDecl {
public readonly List<DatatypeCtor/*!*/>/*!*/ Ctors;
[ContractInvariantMethod]
@@ -1698,7 +1698,7 @@ namespace Microsoft.Dafny { Contract.Invariant(Mod == null || cce.NonNullElements(Mod));
}
public LoopStmt(IToken tok, List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/>/*!*/ mod)
- : base(tok)
+ : base(tok)
{
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(invariants));
@@ -2564,7 +2564,7 @@ namespace Microsoft.Dafny { public List<BoundedPool> Bounds; // initialized and filled in by resolver
// invariant Bounds == null || Bounds.Count == BoundVars.Count;
- public List<BoundVar> MissingBounds; // filled in during resolution; remains "null" if bounds can be found
+ public List<BoundVar> MissingBounds; // filled in during resolution; remains "null" if bounds can be found
// invariant Bounds == null || MissingBounds == null;
public ComprehensionExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression range, Expression/*!*/ term, Attributes attrs)
@@ -2582,7 +2582,7 @@ namespace Microsoft.Dafny { public override IEnumerable<Expression> SubExpressions {
get {
if (Range != null) { yield return Range; }
- yield return Term;
+ yield return Term;
}
}
}
|