chore: cleanup deprecations (#89)

* . * chore: remove deprecated `html!` tactic --------- Co-authored-by: Wojciech Nawrocki <[email protected]>
leanprover-community · Nov 24, 2024 · 5f1a4a0 · 5f1a4a0
1 parent 4546ff0
commit 5f1a4a0
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 25 deletions.
diff --git a/ProofWidgets/Component/HtmlDisplay.lean b/ProofWidgets/Component/HtmlDisplay.lean
@@ -71,16 +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]
-syntax (name := htmlTac) "html! " term : tactic
-
-open Tactic in
-@[tactic htmlTac]
-def elabHtmlTac : Tactic | _ => pure ()
-
 end HtmlCommand
 end ProofWidgets
 

diff --git a/ProofWidgets/Presentation/Expr.lean b/ProofWidgets/Presentation/Expr.lean
@@ -81,21 +81,6 @@ structure GetExprPresentationParams where
   name : Name
   deriving RpcEncodable
 
-@[server_rpc_method]
-def getExprPresentation : GetExprPresentationParams → RequestM (RequestTask Html)
-  | { expr := ⟨expr⟩, name } => RequestM.asTask do
-    let ci := expr.ci
-    if !exprPresenters.hasTag ci.env name then
-      throw <| RequestError.invalidParams s!"The constant '{name}' is not an Expr presenter."
-    match evalExprPresenter ci.env ci.options name with
-    | .ok p =>
-      expr.runMetaM p.present
-    | .error e =>
-      throw <| RequestError.internalError s!"Failed to evaluate Expr presenter '{name}': {e}"
-
--- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/deprecation.20warning.20from.20ProofWidgets
-attribute [deprecated] getExprPresentation
-
 structure ExprPresentationProps where
   expr : WithRpcRef ExprWithCtx
   deriving RpcEncodable