chore: remove StrategyAttrs

src/Lean/Elab.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 import Lean.Elab.Import
 import Lean.Elab.Exception
-import Lean.Elab.StrategyAttrs
 import Lean.Elab.Command
 import Lean.Elab.Term
 import Lean.Elab.App

src/Lean/Elab/StrategyAttrs.lean

@@ -1,30 +0,0 @@
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-import Lean.Attributes
-
-namespace Lean
-/-
-Elaborator strategies available in the Lean3 elaborator.
-We want to support a more general approach, but we need to provide
-the strategy selection attributes while we rely on the Lean3 elaborator.
--/
-inductive ElaboratorStrategy
-  | simple | withExpectedType | asEliminator
-
-instance : Inhabited ElaboratorStrategy :=
-  ⟨ElaboratorStrategy.withExpectedType⟩
-
-builtin_initialize elaboratorStrategyAttrs : EnumAttributes ElaboratorStrategy ←
-  registerEnumAttributes `elaboratorStrategy
-    [(`elabWithExpectedType, "instructs elaborator that the arguments of the function application (f ...) should be elaborated using information about the expected type", ElaboratorStrategy.withExpectedType),
-     (`elabSimple, "instructs elaborator that the arguments of the function application (f ...) should be elaborated from left to right, and without propagating information from the expected type to its arguments", ElaboratorStrategy.simple),
-     (`elabAsEliminator, "instructs elaborator that the arguments of the function application (f ...) should be elaborated as f were an eliminator", ElaboratorStrategy.asEliminator)]
-
-@[export lean_get_elaborator_strategy]
-def getElaboratorStrategy (env : Environment) (n : Name) : Option ElaboratorStrategy :=
-  elaboratorStrategyAttrs.getValue env n
-
-end Lean