chore: remove deprecated html! tactic

leanprover-community · Nov 24, 2024 · 3cc4cd1 · 3cc4cd1
1 parent 3e785b6
commit 3cc4cd1
Showing 1 changed file with 0 additions and 12 deletions.
diff --git a/ProofWidgets/Component/HtmlDisplay.lean b/ProofWidgets/Component/HtmlDisplay.lean
@@ -71,18 +71,6 @@ def elabHtmlCmd : CommandElab := fun
       stx
   | stx => throwError "Unexpected syntax {stx}."
 
-/-- The `html!` tactic is deprecated and does nothing.
-If you have a use for it,
-please open an issue on https://github.com/leanprover-community/ProofWidgets4. -/
-@[deprecated "The `html!` tactic is deprecated and does nothing. If you have a use for it, \
-  please open an issue on https://github.com/leanprover-community/ProofWidgets4."
-  (since := "2024-05-15")]
-syntax (name := htmlTac) "html! " term : tactic
-
-open Tactic in
-@[tactic htmlTac]
-def elabHtmlTac : Tactic | _ => pure ()
-
 end HtmlCommand
 end ProofWidgets