chore(tactic): fix tactic doc tags (#12131)

Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
leanprover-community · Feb 21, 2022 · b04851f · b04851f
1 parent 8b93d3a
commit b04851f
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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