chore: fix definitions

See commit before update stage0 for explanation.

src/Lean/Compiler/NameMangling.lean

@@ -41,7 +41,7 @@ private def Name.mangleAux : Name → String
     let m := String.mangle s
     match p with
     | Name.anonymous => m
-    | _              => mangleAux p ++ "_" ++ m
+    | p              => mangleAux p ++ "_" ++ m
   | Name.num p n _ => mangleAux p ++ "_" ++ toString n ++ "_"
 
 @[export lean_name_mangle]

src/Lean/Elab/Tactic/Basic.lean

@@ -100,8 +100,8 @@ private def evalTacticUsing (s : SavedState) (stx : Syntax) (tactics : List Tact
       catch
       | ex@(Exception.error _ _) =>
         match evalFns with
-        | [] => throw ex
-        | _  => s.restore; loop evalFns
+        | []      => throw ex
+        | evalFns => s.restore; loop evalFns
       | ex@(Exception.internal id) =>
         if id == unsupportedSyntaxExceptionId then
           s.restore; loop evalFns

src/Lean/Meta/Match/CaseValues.lean

@@ -96,7 +96,7 @@ let rec loop : Nat → MVarId → List Expr → Array FVarId → Array CaseValue
     | [] => do
       appendTagSuffix elseSubgoal.mvarId ((`case).appendIndexAfter (i+1))
       pure $ subgoals.push { mvarId := elseSubgoal.mvarId, newHs := hs.push elseSubgoal.newH, subst := {} }
-    | _  => loop (i+1) elseSubgoal.mvarId vs (hs.push elseSubgoal.newH) subgoals
+    | vs => loop (i+1) elseSubgoal.mvarId vs (hs.push elseSubgoal.newH) subgoals
 loop 1 mvarId values.toList #[] #[]
 
 end Lean.Meta