From 00793fcdd8d76ed82e7bd03825ba7cd4d80b67ff Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Tue, 13 Sep 2022 15:20:23 +0200
Subject: [PATCH] chore: remove old bootstrapping hack

---
 src/Lean/Elab/Declaration.lean | 12 +++---------
 1 file changed, 3 insertions(+), 9 deletions(-)

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