From fd8fb3cf9eeb8d46ade8e376f4d4961e43b4af16 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 16 Sep 2021 07:41:04 -0700
Subject: [PATCH] chore: prepare to change `simp` syntax

---
 src/Lean/Elab/Tactic/Simp.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index fdc02c5892..12330a63fb 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/src/Lean/Elab/Tactic/Simp.lean
@@ -126,14 +126,14 @@ structure MkSimpContextResult where
 
 --  If `ctx == false`, the argument is assumed to have type `Meta.Simp.Config`, and `Meta.Simp.ConfigCtx` otherwise. -/
 def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (ctx := false) (ignoreStarArg : Bool := false) : TacticM MkSimpContextResult := do
-  let simpOnly := !stx[2].isNone
+  let simpOnly := !stx[3].isNone
   let simpLemmas ←
     if simpOnly then
       ({} : SimpLemmas).addConst ``eq_self
     else
       getSimpLemmas
   let congrLemmas ← getCongrLemmas
-  let r ← elabSimpArgs stx[3] (eraseLocal := eraseLocal) {
+  let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) {
     config      := (← elabSimpConfig stx[1] (ctx := ctx))
     simpLemmas, congrLemmas
   }
@@ -157,12 +157,12 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (ctx := false) (ignoreStarA
     return { ctx, fvarIdToLemmaId }
 
 /-
-  "simp " ("(" "config" ":=" term ")")? ("only ")? ("[" simpLemma,* "]")? (location)?
+  "simp " (config)? (discharger)? ("only ")? ("[" simpLemma,* "]")? (location)?
 -/
 @[builtinTactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => do
   let { ctx, fvarIdToLemmaId } ← withMainContext <| mkSimpContext stx (eraseLocal := false)
   -- trace[Meta.debug] "Lemmas {← toMessageData ctx.simpLemmas.post}"
-  let loc := expandOptLocation stx[4]
+  let loc := expandOptLocation stx[5]
   match loc with
   | Location.targets hUserNames simplifyTarget =>
     withMainContext do