Skip to content

Commit

Permalink
Fixed traitDecl
Browse files Browse the repository at this point in the history
  • Loading branch information
MikaelMayer committed Oct 10, 2024
1 parent 4c602ce commit 8aa0335
Showing 1 changed file with 2 additions and 3 deletions.
5 changes: 2 additions & 3 deletions Source/DafnyCore/Dafny.atg
Original file line number Diff line number Diff line change
Expand Up @@ -574,7 +574,6 @@ TraitDecl<DeclModifierData dmodIn, ModuleDefinition/*!*/ module, out TraitDecl/*
CheckDeclModifiers(ref dmodIn, "trait", AllowedDeclModifiers.None);
IToken/*!*/ tokenWithTrailingDocString;
List<Type> parentTraits = new List<Type>();
Attributes attrs = null;
bool isRefining = false;
List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>(); //traits should not support type parameters at the moment
List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
Expand All @@ -583,7 +582,7 @@ TraitDecl<DeclModifierData dmodIn, ModuleDefinition/*!*/ module, out TraitDecl/*
.)
SYNC
"trait" (. CheckAndSetTokenOnce(ref dmodIn.FirstTokenExceptAttributes); .)
{ Attribute<ref attrs> }
{ Attribute<ref dmodIn.Attributes> }
ClassName<out var name> (. tokenWithTrailingDocString = t; .)
[ GenericParameters<typeArgs, true> ] (. tokenWithTrailingDocString = t; .)
[ ExtendsClause<parentTraits, out tokenWithTrailingDocString, null>
Expand All @@ -595,7 +594,7 @@ TraitDecl<DeclModifierData dmodIn, ModuleDefinition/*!*/ module, out TraitDecl/*
ClassMemberDecl<dmod, members, true, false>
}
"}"
(. trait = new TraitDecl(new RangeToken(dmodIn.FirstToken, t), name, module, typeArgs, members, attrs, isRefining, parentTraits);
(. trait = new TraitDecl(new RangeToken(dmodIn.FirstToken, t), name, module, typeArgs, members, dmodIn.Attributes, isRefining, parentTraits);
trait.BodyStartTok = bodyStart;
trait.TokenWithTrailingDocString = tokenWithTrailingDocString;
.)
Expand Down

0 comments on commit 8aa0335

Please sign in to comment.