diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index 8f6d2a2c55..e5247d0fea 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/src/Lean/Elab/Declaration.lean @@ -159,15 +159,9 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Comm addDocString' ctorName ctorModifiers.docString? addAuxDeclarationRanges ctorName ctor ctor[2] return { ref := ctor, modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView } - let mut computedFields := #[] - let mut classes := #[] - if decl.getNumArgs == 6 then - -- TODO: remove after stage0 update - classes ← getOptDerivingClasses decl[5] - else - computedFields ← (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do - return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := ⟨cf[3]⟩, matchAlts := ⟨cf[4]⟩ } - classes ← getOptDerivingClasses decl[6] + let computedFields ← (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do + return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := ⟨cf[3]⟩, matchAlts := ⟨cf[4]⟩ } + let classes ← getOptDerivingClasses decl[6] return { ref := decl shortDeclName := name