From a29a61b728a4cf8cc682ef84969529f032cf42e5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 19 Aug 2022 11:56:22 -0700
Subject: [PATCH] chore: remove dead code

---
 src/Lean/Compiler/CompilerM.lean | 17 -----------------
 src/Lean/Compiler/Simp.lean      | 17 -----------------
 tests/lean/run/lcnf1.lean        |  2 +-
 3 files changed, 1 insertion(+), 35 deletions(-)

diff --git a/src/Lean/Compiler/CompilerM.lean b/src/Lean/Compiler/CompilerM.lean
index 73c0f39241..216210dccf 100644
--- a/src/Lean/Compiler/CompilerM.lean
+++ b/src/Lean/Compiler/CompilerM.lean
@@ -38,23 +38,6 @@ instance : MonadInferType CompilerM where
 instance : MonadLCtx CompilerM where
   getLCtx := return (← get).lctx
 
-structure CompilerM.SavedState where
-  core     : Core.State
-  compiler : CompilerM.State
-  deriving Inhabited
-
-protected def CompilerM.saveState : CompilerM CompilerM.SavedState :=
-  return { core := (← getThe Core.State), compiler := (← get) }
-
-/-- Restore backtrackable parts of the state. -/
-def CompilerM.SavedState.restore (b : SavedState) : CompilerM Unit := do
-  Core.restore b.core
-  set b.compiler
-
-instance : MonadBacktrack CompilerM.SavedState CompilerM where
-  saveState      := CompilerM.saveState
-  restoreState s := s.restore
-
 /--
 Add a new local declaration with the given arguments to the `LocalContext` of `CompilerM`.
 Returns the free variable representing the new declaration.
diff --git a/src/Lean/Compiler/Simp.lean b/src/Lean/Compiler/Simp.lean
index 85d2b55d43..0050f63c8d 100644
--- a/src/Lean/Compiler/Simp.lean
+++ b/src/Lean/Compiler/Simp.lean
@@ -121,23 +121,6 @@ structure State where
 
 abbrev SimpM := ReaderT Context $ StateRefT State CompilerM
 
-structure SavedState where
-  compiler : CompilerM.SavedState
-  simp : State
-  deriving Inhabited
-
-protected def saveState : SimpM SavedState :=
-  return { compiler := (← CompilerM.saveState), simp := (← get) }
-
-/-- Restore backtrackable parts of the state. -/
-def SavedState.restore (b : SavedState) : SimpM Unit := do
-  b.compiler.restore
-  set b.simp
-
-instance : MonadBacktrack SavedState SimpM where
-  saveState      := Simp.saveState
-  restoreState s := s.restore
-
 def markSimplified : SimpM Unit :=
   modify fun s => { s with simplified := true }
 
diff --git a/tests/lean/run/lcnf1.lean b/tests/lean/run/lcnf1.lean
index cba6cc39d1..c399bf0796 100644
--- a/tests/lean/run/lcnf1.lean
+++ b/tests/lean/run/lcnf1.lean
@@ -44,7 +44,7 @@ def Vec.head : Vec α (n+1) → α
 #eval Compiler.compile #[``Lean.Elab.Term.synthesizeSyntheticMVars]
 
 set_option profiler true
-set_option trace.Compiler true
+set_option trace.Compiler.simp true
 #eval Compiler.compile #[``Lean.Meta.isExprDefEqAuxImpl]
 
 def foo (a b : Nat) :=