docs(*): merge rewrite tactic tag into rewriting (#2512)

We had two overlapping tags in the docs. Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
leanprover-community · Apr 24, 2020 · 00d7da2 · 00d7da2
1 parent 13393e3
commit 00d7da2
Show file tree

Hide file tree

Showing 6 changed files with 7 additions and 7 deletions.
diff --git a/src/tactic/converter/apply_congr.lean b/src/tactic/converter/apply_congr.lean
@@ -94,7 +94,7 @@ add_tactic_doc {
   name := "apply_congr",
   category := doc_category.tactic,
   decl_names := [`conv.interactive.apply_congr],
-  tags := ["conv", "congruence", "rewrite"]
+  tags := ["conv", "congruence", "rewriting"]
 }
 
 end conv.interactive
diff --git a/src/tactic/elide.lean b/src/tactic/elide.lean
@@ -82,7 +82,7 @@ add_tactic_doc
 { name        := "elide / unelide",
   category    := doc_category.tactic,
   decl_names  := [`tactic.interactive.elide, `tactic.interactive.unelide],
-  tags        := ["goal management", "context management", "rewrite"] }
+  tags        := ["goal management", "context management", "rewriting"] }
 
 end interactive
 

diff --git a/src/tactic/ext.lean b/src/tactic/ext.lean
@@ -396,6 +396,6 @@ add_tactic_doc
 { name        := "ext1 / ext",
   category    := doc_category.tactic,
   decl_names  := [`tactic.interactive.ext1, `tactic.interactive.ext],
-  tags        := ["rewrite", "logic"] }
+  tags        := ["rewriting", "logic"] }
 
 end tactic
diff --git a/src/tactic/interactive.lean b/src/tactic/interactive.lean
@@ -42,7 +42,7 @@ add_tactic_doc
 { name       := "substs",
   category   := doc_category.tactic,
   decl_names := [`tactic.interactive.substs],
-  tags       := ["rewrite"] }
+  tags       := ["rewriting"] }
 
 /-- Unfold coercion-related definitions -/
 meta def unfold_coes (loc : parse location) : tactic unit :=

diff --git a/src/tactic/lean_core_docs.lean b/src/tactic/lean_core_docs.lean
@@ -576,13 +576,13 @@ add_tactic_doc
 { name       := "subst",
   category   := doc_category.tactic,
   decl_names := [`tactic.interactive.subst],
-  tags       := ["core", "rewrite"] }
+  tags       := ["core", "rewriting"] }
 
 add_tactic_doc
 { name       := "subst_vars",
   category   := doc_category.tactic,
   decl_names := [`tactic.interactive.subst_vars],
-  tags       := ["core", "rewrite"] }
+  tags       := ["core", "rewriting"] }
 
 add_tactic_doc
 { name       := "success_if_fail",

diff --git a/src/tactic/rewrite.lean b/src/tactic/rewrite.lean
@@ -207,7 +207,7 @@ add_tactic_doc
 { name                     := "assoc_rewrite",
   category                 := doc_category.tactic,
   decl_names               := [`tactic.interactive.assoc_rewrite, `tactic.interactive.assoc_rw],
-  tags                     := ["rewrite"],
+  tags                     := ["rewriting"],
   inherit_description_from := `tactic.interactive.assoc_rewrite }
 
 end interactive