fix: make sure simp only still uses eq_self

src/Lean/Elab/Tactic/Simp.lean

@@ -139,10 +139,15 @@ structure MkSimpContextResult where
 --  If `ctx == false`, the argument is assumed to have type `Meta.Simp.Config`, and `Meta.Simp.ConfigCtx` otherwise. -/
 private def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (ctx := false) (ignoreStarArg : Bool := false) : TacticM MkSimpContextResult := do
   let simpOnly := !stx[2].isNone
+  let simpLemmas ←
+    if simpOnly then
+      ({} : SimpLemmas).addConst ``eq_self
+    else
+      getSimpLemmas
+  let congrLemmas ← getCongrLemmas
   let r ← elabSimpArgs stx[3] (eraseLocal := eraseLocal) {
     config      := (← elabSimpConfig stx[1] (ctx := ctx))
-    simpLemmas  := if simpOnly then {} else (← getSimpLemmas)
-    congrLemmas := (← getCongrLemmas)
+    simpLemmas, congrLemmas
   }
   if !r.starArg || ignoreStarArg then
     return { r with fvarIdToLemmaId := {} }

tests/lean/run/setOptionTermTactic.lean

@@ -7,4 +7,3 @@ theorem ex : f = g := by
   simp only [f]
   set_option trace.Meta.Tactic.simp true in simp only [Nat.add_succ, g]
   simp only [Nat.zero_add]
-  rfl

tests/lean/run/simpOnly.lean

@@ -11,3 +11,8 @@ theorem ex3 (n m : Nat) : 0 + (n, m).1 + 0 = n := by
 
 theorem ex4 (n m : Nat) : 0 + (n, m).1 + 0 = n := by
   simp
+
+theorem ex5 (m n : Nat) : m + n = n + m := by
+  induction n with
+  | zero      => rw [Nat.zero_add, Nat.add_zero]
+  | succ n ih => simp only [Nat.add_succ, Nat.succ_add, ih]