From ded9572c508b41dbf9402d39b3875dd4e967ad86 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Wed, 20 Jan 2021 11:24:14 -0800
Subject: Fix: "tactic" is not a tactic, so can't begin a .. tacn::

---
 doc/sphinx/proofs/writing-proofs/rewriting.rst | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index 8873d02888..8c8c88c526 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -890,10 +890,8 @@ the conversion in hypotheses :n:`{+ @ident}`.
 Conversion tactics applied to hypotheses
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. tacn:: @tactic in {+, @ident}
-
-   Applies :token:`tactic` (any of the conversion tactics listed in this
-   section) to the hypotheses :n:`{+ @ident}`.
+   The form :n:`@tactic in {+, @ident }` applies :token:`tactic` (any of the
+   conversion tactics listed in this section) to the hypotheses :n:`{+ @ident}`.
 
    If :token:`ident` is a local definition, then :token:`ident` can be replaced by
    :n:`type of @ident` to address not the body but the type of the local
-- 
cgit v1.2.3