From 83fb51f601a1e349ff23f2d4a3cb1e08a52ef7ec Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 2 Nov 2020 06:39:21 -0800
Subject: [PATCH] chore: remove `StrategyAttrs`

---
 src/Lean/Elab.lean               |  1 -
 src/Lean/Elab/StrategyAttrs.lean | 30 ------------------------------
 2 files changed, 31 deletions(-)
 delete mode 100644 src/Lean/Elab/StrategyAttrs.lean

diff --git a/src/Lean/Elab.lean b/src/Lean/Elab.lean
index b6d22aa99b..e884462a60 100644
--- a/src/Lean/Elab.lean
+++ b/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
diff --git a/src/Lean/Elab/StrategyAttrs.lean b/src/Lean/Elab/StrategyAttrs.lean
deleted file mode 100644
index beefc14f42..0000000000
--- a/src/Lean/Elab/StrategyAttrs.lean
+++ /dev/null
@@ -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