chore: remove LazyInitExtension

leanprover · Oct 8, 2024 · 9807459 · 9807459
1 parent 7c29c3f
commit 9807459
Show file tree

Hide file tree

Showing 3 changed files with 0 additions and 44 deletions.
diff --git a/src/Lean.lean b/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

diff --git a/src/Lean/LazyInitExtension.lean b/src/Lean/LazyInitExtension.lean
diff --git a/src/Lean/Meta/Tactic/SplitIf.lean b/src/Lean/Meta/Tactic/SplitIf.lean
@@ -4,7 +4,6 @@ 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