Merge PR #9896: Minor correction to numeral notations doc

Reviewed-by: Zimmi48

1 files changed, 6 insertions, 6 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 1e201953b3..7a5d07b2b7 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1522,9 +1522,9 @@ Numeral notations
    .. exn:: Unexpected term @term while parsing a numeral notation.
 
      Parsing functions must always return ground terms, made up of
-     applications of constructors and inductive types.  Parsing
-     functions may not return terms containing axioms, bare
-     (co)fixpoints, lambdas, etc.
+     applications of constructors, inductive types, and primitive
+     integers.  Parsing functions may not return terms containing
+     axioms, bare (co)fixpoints, lambdas, etc.
 
    .. exn:: Unexpected non-option term @term while parsing a numeral notation.
 
@@ -1650,9 +1650,9 @@ String notations
    .. exn:: Unexpected term @term while parsing a string notation.
 
      Parsing functions must always return ground terms, made up of
-     applications of constructors and inductive types.  Parsing
-     functions may not return terms containing axioms, bare
-     (co)fixpoints, lambdas, etc.
+     applications of constructors, inductive types, and primitive
+     integers.  Parsing functions may not return terms containing
+     axioms, bare (co)fixpoints, lambdas, etc.
 
    .. exn:: Unexpected non-option term @term while parsing a string notation.