From f7ab307779e4d21d706be13acad670d63d0e6537 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Wed, 2 Dec 2015 12:35:54 -0800 Subject: Fix issue 110. Set useImport to true when trying to registerTopLevelDecls in MakeAbstractSignature. --- Source/Dafny/Resolver.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Source') diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 52845c3f..9dc0f829 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1269,7 +1269,7 @@ namespace Microsoft.Dafny foreach (var kv in p.TopLevels) { mod.TopLevelDecls.Add(CloneDeclaration(kv.Value, mod, mods, Name)); } - var sig = RegisterTopLevelDecls(mod, false); + var sig = RegisterTopLevelDecls(mod, true); sig.Refines = p.Refines; sig.CompileSignature = p; sig.IsAbstract = p.IsAbstract; -- cgit v1.2.3