From 2a393cd4abdf4e985397279f3453448e1a406ad4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 22 Oct 2020 07:06:09 -0700
Subject: [PATCH] chore: remove workaround

---
 src/Lean/Attributes.lean | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean
index 894877ae49..dd00c3b92f 100644
--- a/src/Lean/Attributes.lean
+++ b/src/Lean/Attributes.lean
@@ -43,8 +43,6 @@ structure AttributeImplCore :=
 
 structure AttributeImpl extends AttributeImplCore :=
   (add (decl : Name) (args : Syntax) (persistent : Bool) : AttrM Unit)
-  -- TODO: shouldn't be necessary
-  (applicationTime := AttributeApplicationTime.afterTypeChecking)
 
 instance : Inhabited AttributeImpl :=
   ⟨{ name := arbitrary _, descr := arbitrary _, add := fun env _ _ _ => pure () }⟩
@@ -323,8 +321,6 @@ structure ParametricAttributeImpl (α : Type) extends AttributeImplCore :=
   (getParam : Name → Syntax → AttrM α)
   (afterSet : Name → α → AttrM Unit := fun env _ _ => pure ())
   (afterImport : Array (Array (Name × α)) → ImportM Unit := fun _ => pure ())
-  -- TODO: shouldn't be necessary
-  (applicationTime := AttributeApplicationTime.afterTypeChecking)
 
 def registerParametricAttribute {α : Type} [Inhabited α] (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do
   let ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← registerPersistentEnvExtension {