From 2012d9dca16c0419f051bc0679967e6a587f0ca4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 30 Aug 2021 09:48:39 -0700
Subject: [PATCH] fix: make sure `simp only` still uses `eq_self`

---
 src/Lean/Elab/Tactic/Simp.lean          | 9 +++++++--
 tests/lean/run/setOptionTermTactic.lean | 1 -
 tests/lean/run/simpOnly.lean            | 5 +++++
 3 files changed, 12 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index e7fb809a79..d3b9203262 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/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 := {} }
diff --git a/tests/lean/run/setOptionTermTactic.lean b/tests/lean/run/setOptionTermTactic.lean
index 3195f9d55f..8089af352a 100644
--- a/tests/lean/run/setOptionTermTactic.lean
+++ b/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
diff --git a/tests/lean/run/simpOnly.lean b/tests/lean/run/simpOnly.lean
index c39a6d7176..358d28605c 100644
--- a/tests/lean/run/simpOnly.lean
+++ b/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]