diff --git a/src/tactic/linear_combination.lean b/src/tactic/linear_combination.lean index 0528cca0926de..dccfc624c581f 100644 --- a/src/tactic/linear_combination.lean +++ b/src/tactic/linear_combination.lean @@ -388,7 +388,7 @@ add_tactic_doc { name := "linear_combination", category := doc_category.tactic, decl_names := [`tactic.interactive.linear_combination], - tags := [] } + tags := ["arithmetic"] } end interactive_mode end linear_combo diff --git a/src/tactic/rewrite_search/frontend.lean b/src/tactic/rewrite_search/frontend.lean index a5dbd4bf0b260..a3f8b4b7a9d5c 100644 --- a/src/tactic/rewrite_search/frontend.lean +++ b/src/tactic/rewrite_search/frontend.lean @@ -82,6 +82,6 @@ add_tactic_doc { name := "rewrite_search", category := doc_category.tactic, decl_names := [`tactic.interactive.rewrite_search], - tags := ["rewrite", "automation"] } + tags := ["rewriting", "automation"] } end tactic.interactive