summaryrefslogtreecommitdiff
path: root/Source/Dafny/Translator.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Dafny/Translator.cs')
-rw-r--r--Source/Dafny/Translator.cs2
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 4199157e..ca30c88c 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1242,7 +1242,7 @@ namespace Microsoft.Dafny {
//this adds: function implements$J(ClassName): bool;
if (c is TraitDecl)
{
- var arg_ref = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.Ty), true);
+ var arg_ref = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), true);
var res = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
var implement_intr = new Bpl.Function(c.tok, "implements$" + c.Name, new List<Variable> { arg_ref }, res);
sink.TopLevelDeclarations.Add(implement_intr);