From dadab540149678f92f34729e79cb357ea6dd2ec9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 29 Jul 2022 20:41:30 -0700
Subject: [PATCH] chore: remove unused param

---
 src/Lean/Elab/Arg.lean        | 6 ++----
 src/Lean/Elab/PatternVar.lean | 2 +-
 2 files changed, 3 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Elab/Arg.lean b/src/Lean/Elab/Arg.lean
index eaeab846cb..a0ebb526c5 100644
--- a/src/Lean/Elab/Arg.lean
+++ b/src/Lean/Elab/Arg.lean
@@ -30,8 +30,7 @@ def addNamedArg (namedArgs : Array NamedArg) (namedArg : NamedArg) : MetaM (Arra
     throwError "argument '{namedArg.name}' was already set"
   return namedArgs.push namedArg
 
-set_option linter.unusedVariables.funArgs false in
-partial def expandArgs (args : Array Syntax) (pattern := false) : MetaM (Array NamedArg × Array Arg × Bool) := do
+partial def expandArgs (args : Array Syntax) : MetaM (Array NamedArg × Array Arg × Bool) := do
   let (args, ellipsis) :=
     if args.isEmpty then
       (args, false)
@@ -52,8 +51,7 @@ partial def expandArgs (args : Array Syntax) (pattern := false) : MetaM (Array N
       return (namedArgs, args.push $ Arg.stx stx)
   return (namedArgs, args, ellipsis)
 
-set_option linter.unusedVariables.funArgs false in
-def expandApp (stx : Syntax) (pattern := false) : MetaM (Syntax × Array NamedArg × Array Arg × Bool) := do
+def expandApp (stx : Syntax) : MetaM (Syntax × Array NamedArg × Array Arg × Bool) := do
   let (namedArgs, args, ellipsis) ← expandArgs stx[1].getArgs
   return (stx[0], namedArgs, args, ellipsis)
 
diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean
index 07f8e9bf96..93cf408bf6 100644
--- a/src/Lean/Elab/PatternVar.lean
+++ b/src/Lean/Elab/PatternVar.lean
@@ -217,7 +217,7 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
 where
 
   processCtorApp (stx : Syntax) : M Syntax := do
-    let (f, namedArgs, args, ellipsis) ← expandApp stx true
+    let (f, namedArgs, args, ellipsis) ← expandApp stx
     if f.getKind == ``Parser.Term.dotIdent then
       let namedArgsNew ← namedArgs.mapM fun
         | { ref, name, val := Arg.stx arg } => withRef ref do `(Lean.Parser.Term.namedArgument| ($(mkIdentFrom ref name) := $(← collect arg)))