chore: remove dead code at Structure.lean

src/Lean/Elab/Structure.lean

@@ -82,15 +82,6 @@ def StructFieldInfo.isSubobject (info : StructFieldInfo) : Bool :=
   | StructFieldKind.subobject => true
   | _                         => false
 
-structure ElabStructResult where
-  decl            : Declaration
-  projInfos       : List ProjectionInfo
-  projInstances   : List Name -- projections (to parent classes) that must be marked as instances.
-  mctx            : MetavarContext
-  lctx            : LocalContext
-  localInsts      : LocalInstances
-  defaultAuxDecls : Array (Name × Expr × Expr)
-
 private def defaultCtorName := `mk
 
 /-

src/Lean/Parser/Term.lean

@@ -870,7 +870,7 @@ def matchExprElseAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (ho
 def matchExprAlts (rhsParser : Parser) :=
   leading_parser withPosition $
     many (ppLine >> checkColGe "irrelevant" >> notFollowedBy (symbol "| " >> " _ ") "irrelevant" >> matchExprAlt rhsParser)
-    >> (ppLine >> checkColGe "else-alternative for `match_expr`, i.e., `| _ => ...`" >> matchExprElseAlt rhsParser)
+    >> (ppLine >> checkColGe "irrelevant" >> matchExprElseAlt rhsParser)
 @[builtin_term_parser] def matchExpr := leading_parser:leadPrec
   "match_expr " >> termParser >> " with" >> ppDedent (matchExprAlts termParser)
 

tests/lean/3989_1.lean

@@ -1,3 +0,0 @@
-def foo (ty : Expr) : MetaM Expr :=
-  match_expr ty with
-  | Nat => sorry

tests/lean/3989_1.lean.expected.out

@@ -1 +0,0 @@
-3989_1.lean:4:0: error: expected else-alternative for `match_expr`, i.e., `| _ => ...`

tests/lean/3989_2.lean

@@ -1,6 +0,0 @@
-def foo (ty : Expr) : MetaM Expr :=
-  match_expr ty with
-  | Nat => sorry
-  | BitVec n => sorry
-
-#check Nat

tests/lean/3989_2.lean.expected.out

@@ -1,2 +0,0 @@
-3989_2.lean:6:0: error: expected else-alternative for `match_expr`, i.e., `| _ => ...`
-Nat : Type