Dafny: updated contracts to allow null parent (of the default module)

1 files changed, 1 insertions, 3 deletions

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index f6ba6014..ee4592ce 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -916,15 +916,13 @@ namespace Microsoft.Dafny {
     public readonly List<TypeParameter/*!*/>/*!*/ TypeArgs;

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(Module != null);

       Contract.Invariant(cce.NonNullElements(TypeArgs));

     }

 

-    public TopLevelDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDefinition/*!*/ module, List<TypeParameter/*!*/>/*!*/ typeArgs, Attributes attributes)

+    public TopLevelDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDefinition module, List<TypeParameter/*!*/>/*!*/ typeArgs, Attributes attributes)

       : base(tok, name, attributes) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

-      Contract.Requires(module != null);

       Contract.Requires(cce.NonNullElements(typeArgs));

       Module = module;

       TypeArgs = typeArgs;