chore: remove SplitIf.ext cache

src/Lean.lean

@@ -30,7 +30,6 @@ import Lean.Server
 import Lean.ScopedEnvExtension
 import Lean.DocString
 import Lean.DeclarationRange
-import Lean.LazyInitExtension
 import Lean.LoadDynlib
 import Lean.Widget
 import Lean.Log

src/Lean/Meta/Tactic/SplitIf.lean

@@ -4,31 +4,26 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.LazyInitExtension
 import Lean.Meta.Tactic.Cases
 import Lean.Meta.Tactic.Simp.Main
 
 namespace Lean.Meta
 namespace SplitIf
 
-builtin_initialize ext : LazyInitExtension MetaM Simp.Context ←
-  registerLazyInitExtension do
-    let mut s : SimpTheorems := {}
-    s ← s.addConst ``if_pos
-    s ← s.addConst ``if_neg
-    s ← s.addConst ``dif_pos
-    s ← s.addConst ``dif_neg
-    return {
-      simpTheorems  := #[s]
-      congrTheorems := (← getSimpCongrTheorems)
-      config        := { Simp.neutralConfig with dsimp := false }
-    }
-
 /--
   Default `Simp.Context` for `simpIf` methods. It contains all congruence theorems, but
   just the rewriting rules for reducing `if` expressions. -/
-def getSimpContext : MetaM Simp.Context :=
-  ext.get
+def getSimpContext : MetaM Simp.Context := do
+  let mut s : SimpTheorems := {}
+  s ← s.addConst ``if_pos
+  s ← s.addConst ``if_neg
+  s ← s.addConst ``dif_pos
+  s ← s.addConst ``dif_neg
+  return {
+    simpTheorems  := #[s]
+    congrTheorems := (← getSimpCongrTheorems)
+    config        := { Simp.neutralConfig with dsimp := false }
+  }
 
 /--
   Default `discharge?` function for `simpIf` methods.