Skip to content

Commit c39c5b5

Browse files
committed
chore: post stage0 cleanup for leanprover#8671
1 parent e83b768 commit c39c5b5

File tree

1 file changed

+0
-4
lines changed

1 file changed

+0
-4
lines changed

src/Lean/Elab/Structure.lean

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -353,10 +353,6 @@ def structFields := leading_parser many (structExplicitBinder <|> struct
353353
def structCtor := leading_parser try (declModifiers >> ident >> " :: ")
354354
-/
355355
def structureSyntaxToView (modifiers : Modifiers) (stx : Syntax) : TermElabM StructView := do
356-
let stx := -- for bootstrap compatibility, remove this after stage0 update
357-
if stx.getNumArgs == 7
358-
then stx.setArgs #[stx[0], stx[1], .node .none ``Parser.Command.optDeclSig #[stx[2], stx[3]], stx[4], stx[5], stx[6]]
359-
else stx
360356
checkValidInductiveModifier modifiers
361357
let isClass := stx[0].getKind == ``Parser.Command.classTk
362358
let modifiers := if isClass then modifiers.addAttr { name := `class } else modifiers

0 commit comments

Comments
 (0)