From 3cc4cd1a2495780516b1e0b59d63461ef90844da Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Sat, 23 Nov 2024 21:40:45 -0500 Subject: [PATCH] chore: remove deprecated `html!` tactic --- ProofWidgets/Component/HtmlDisplay.lean | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/ProofWidgets/Component/HtmlDisplay.lean b/ProofWidgets/Component/HtmlDisplay.lean index 85e8eee..e59c655 100644 --- 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