Convert misc chapters to prodn

1 files changed, 4 insertions, 4 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 1791c53aa8..0c51361b64 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -385,8 +385,8 @@ a :token:`decl_notations` clause after the definition of the (co)inductive type
 (co)recursive term (or after the definition of each of them in case of mutual
 definitions). The exact syntax is given by :n:`@decl_notation` for inductive,
 co-inductive, recursive and corecursive definitions and in :ref:`record-types`
-for records. Note that only syntax modifiers that do not require to add or
-change a parsing rule are accepted.
+for records. Note that only syntax modifiers that do not require adding or
+changing a parsing rule are accepted.
 
    .. insertprodn decl_notations decl_notation
 
@@ -1894,12 +1894,12 @@ Tactic notations allow customizing the syntax of tactics.
         - :tacn:`unfold`, :tacn:`with_strategy`
 
       * - ``constr``
-        - :token:`term`
+        - :token:`one_term`
         - a term
         - :tacn:`exact`
 
       * - ``uconstr``
-        - :token:`term`
+        - :token:`one_term`
         - an untyped term
         - :tacn:`refine`