fix: proper deprecation

leanprover · Sep 9, 2024 · 1a343a6 · 1a343a6
1 parent 18c2d27
commit 1a343a6
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/Lean/Elab/Deriving/Basic.lean b/src/Lean/Elab/Deriving/Basic.lean
@@ -63,6 +63,10 @@ end Term
 
 def DerivingHandler := (typeNames : Array Name) → CommandElabM Bool
 
+/-- Deprecated - `DerivingHandler` no longer assumes arguments -/
+@[deprecated DerivingHandler (since := "2024-09-09")]
+def DerivingHandlerNoArgs := (typeNames : Array Name) → CommandElabM Bool
+
 builtin_initialize derivingHandlersRef : IO.Ref (NameMap (List DerivingHandler)) ← IO.mkRef {}
 
 /-- A `DerivingHandler` is called on the fully qualified names of all types it is running for