From d89f5596833c8f85c5208e24a5d3a87bbee8f564 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 24 Oct 2020 07:23:23 -0700
Subject: [PATCH] chore: fix definitions

See commit before update stage0 for explanation.
---
 src/Lean/Compiler/NameMangling.lean | 2 +-
 src/Lean/Elab/Tactic/Basic.lean     | 4 ++--
 src/Lean/Meta/Match/CaseValues.lean | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Compiler/NameMangling.lean b/src/Lean/Compiler/NameMangling.lean
index d23bc33349..4cfa6c45f3 100644
--- a/src/Lean/Compiler/NameMangling.lean
+++ b/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]
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 6d3c66c5d7..a0d40aa567 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/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
diff --git a/src/Lean/Meta/Match/CaseValues.lean b/src/Lean/Meta/Match/CaseValues.lean
index d3ffc36ef7..d694889e78 100644
--- a/src/Lean/Meta/Match/CaseValues.lean
+++ b/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