Merge PR #15563: Move rewrite_db tactic under "Usage"

Reviewed-by: Zimmi48 Co-authored-by: Zimmi48 <Zimmi48@users.noreply.github.com>
coq · Feb 2, 2022 · 7d14801 · 7d14801
2 parents 297cda7 + f0bd8a8
commit 7d14801
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 4 deletions.
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -785,6 +785,11 @@ Usage
    :tacn:`setoid_rewrite` :n:`@one_term` is basically equivalent to
    :n:`rewrite_strat outermost @one_term`.
 
+
+.. tacn:: rewrite_db @ident__1 {? in @ident__2 }
+
+   Equivalent to :tacn:`rewrite_strat` :n:`(topdown (hints @ident__1)) {? in @ident__2 }`
+
 Definitions
 ~~~~~~~~~~~
 

diff --git a/doc/sphinx/proofs/writing-proofs/equality.rst b/doc/sphinx/proofs/writing-proofs/equality.rst
@@ -233,10 +233,6 @@ Rewriting with Leibniz and setoid equality
    :name: rewrite *; _
    :undocumented:
 
-.. tacn:: rewrite_db @ident {? in @ident }
-
-   Equivalent to :tacn:`rewrite_strat` :n:`(topdown (hints @ident)) in @ident`
-
 .. tacn:: replace @one_term__from with @one_term__to {? @occurrences } {? by @ltac_expr3 }
           replace {? {| -> | <- } } @one_term__from {? @occurrences }
    :name: replace; _