From d6418299c7eb72eb7e933aab41784907f4776640 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 27 Oct 2020 12:56:54 -0700
Subject: [PATCH] chore: naming convention

---
 src/Init/LeanInit.lean          | 2 +-
 src/Lean/Elab/Binders.lean      | 4 ++--
 src/Lean/Elab/Tactic/Match.lean | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean
index b77c68e075..463eb0d7b2 100644
--- a/src/Init/LeanInit.lean
+++ b/src/Init/LeanInit.lean
@@ -248,7 +248,7 @@ def getKind (stx : Syntax) : SyntaxNodeKind :=
   | Syntax.atom _ v      => mkNameSimple v
   | Syntax.ident _ _ _ _ => identKind
 
-def updateKind (stx : Syntax) (k : SyntaxNodeKind) : Syntax :=
+def setKind (stx : Syntax) (k : SyntaxNodeKind) : Syntax :=
   match stx with
   | Syntax.node _ args => Syntax.node k args
   | _                  => stx
diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index b0e94c2b9a..8648fd8cc2 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -507,8 +507,8 @@ def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (useLetExpr : B
     let stxNew ← `(let x : $type := $val; match x with | $pat => $body)
     let stxNew  := match useLetExpr, elabBodyFirst with
       | true,  false => stxNew
-      | true,  true  => stxNew.updateKind `Lean.Parser.Term.«let*»
-      | false, true  => stxNew.updateKind `Lean.Parser.Term.«let!»
+      | true,  true  => stxNew.setKind `Lean.Parser.Term.«let*»
+      | false, true  => stxNew.setKind `Lean.Parser.Term.«let!»
       | false, false => unreachable!
     withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
   else if letDecl.getKind == `Lean.Parser.Term.letEqnsDecl then
diff --git a/src/Lean/Elab/Tactic/Match.lean b/src/Lean/Elab/Tactic/Match.lean
index 75010eb955..9e5f431afe 100644
--- a/src/Lean/Elab/Tactic/Match.lean
+++ b/src/Lean/Elab/Tactic/Match.lean
@@ -17,7 +17,7 @@ private def mkAuxiliaryMatchTermAux (parentTag : Name) (matchTac : Syntax) : Sta
   let matchAlts := matchTac[4]
   let alts      := matchAlts[1].getArgs
   let newAlts ← alts.mapSepElemsM fun alt => do
-    let alt    := alt.updateKind `Lean.Parser.Term.matchAlt
+    let alt    := alt.setKind `Lean.Parser.Term.matchAlt
     let holeOrTacticSeq := alt[2]
     if holeOrTacticSeq.isOfKind `Lean.Parser.Term.syntheticHole then
       pure alt
@@ -33,7 +33,7 @@ private def mkAuxiliaryMatchTermAux (parentTag : Name) (matchTac : Syntax) : Sta
       let newCase ← `(tactic| case $newHoleId => $holeOrTacticSeq:tacticSeq )
       modify fun s => { s with cases := s.cases.push newCase }
       pure $ alt.setArg 2 newHole
-  let result  := matchTac.updateKind `Lean.Parser.Term.«match»
+  let result  := matchTac.setKind `Lean.Parser.Term.«match»
   let result  := result.setArg 4 (matchAlts.setArg 1 (mkNullNode newAlts))
   pure result