From 53b2ceea51b4406c9b102f7f4fee7944db9278ba Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 16 May 2021 13:07:13 -0700
Subject: [PATCH] fix: missing `withoutModifyingState` at `elabSimpConfig`

---
 src/Lean/Elab/Tactic/Simp.lean        |  2 +-
 tests/lean/run/simpDischargeLoop.lean | 17 +++++++++++++++++
 2 files changed, 18 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index f8609346d2..7f295623d7 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/src/Lean/Elab/Tactic/Simp.lean
@@ -31,7 +31,7 @@ def elabSimpConfig (optConfig : Syntax) (ctx : Bool) : TermElabM Meta.Simp.Confi
     else
       return {}
   else
-    withLCtx {} {} <| withNewMCtxDepth <| Term.withSynthesize do
+    withoutModifyingState <| withLCtx {} {} <| Term.withSynthesize do
       let c ← Term.elabTermEnsuringType optConfig[3] (Lean.mkConst (if ctx then ``Meta.Simp.ConfigCtx else ``Meta.Simp.Config))
       if ctx then
         return (← evalSimpConfigCtx (← instantiateMVars c)).toConfig
diff --git a/tests/lean/run/simpDischargeLoop.lean b/tests/lean/run/simpDischargeLoop.lean
index 7f36d509d0..c658e567fb 100644
--- a/tests/lean/run/simpDischargeLoop.lean
+++ b/tests/lean/run/simpDischargeLoop.lean
@@ -26,3 +26,20 @@ theorem double.inj' : double n = double m → n = m := by
       simp
       apply ih
       simp_all [double]
+
+theorem double.inj'' : double n = double m → n = m := by
+  intro h
+  induction n generalizing m with
+  | zero => cases m <;> trivial
+  | succ n ih =>
+    cases m with
+    | zero   => contradiction
+    | succ m =>
+      simp [ih, double]
+      simp [double] at h
+      apply ih h
+
+theorem double.inj''' : double n = double m → n = m := by
+  simp (config := { maxDischargeDepth := 2 })
+  simp (config := { maxSteps := 2000000 })
+  admit