Apply suggestions from code review

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>

doc/sphinx/user-extensions/syntax-extensions.rst

@@ -82,14 +82,14 @@ notations: the start and end of a string token in a notation string
 must be doubled double quotes. Spaces occurring in these strings are
 part of the string symbol and do not contribute to the separation
 between tokens. To refer to double quotes in these strings, use four
-double quotes (e.g. the notation :g:`"A ""I'm a """"infix"""" string symbol"" B"`
+double quotes (e.g. the notation :g:`"A ""I'm an """"infix"""" string symbol"" B"`
 defines an infix notation whose infix symbol is the string
-:g:`"I'm a ""infix"" string symbol"`). Symbols are allowed to contain
+:g:`"I'm an ""infix"" string symbol"`). Symbols may contain
 strings without being strings themselves but such notations can be
 used only for printing (see :ref:`Use of notations for printing <UseOfNotationsForPrinting>`).
-Also, in this case, no spaces is allowed in the symbol and, if the
+In this case, no spaces are allowed in the symbol.  Also, if the
 symbol starts with a double quote, it should be surrounded with single
-quotes to prevent a confusion with the beginning of a string symbol.
+quotes to prevent confusion with the beginning of a string symbol.
 
 A notation binds a syntactic expression to a term. Unless the parser
 and pretty-printer of Coq already know how to deal with the syntactic