From 7a57a23e4fb8a74e8746d4eaee900f2ced37a28a Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 9 Aug 2020 14:25:51 -0700
Subject: Convert misc chapters to prodn

---
 doc/sphinx/user-extensions/syntax-extensions.rst | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'doc/sphinx/user-extensions/syntax-extensions.rst')

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`
 
-- 
cgit v1.2.3