From 5f3663cb57b2e12c498a92bd5d50454d95f6f257 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 3 Apr 2019 00:27:05 -0400
Subject: Minor correction to numeral notations doc

---
 doc/sphinx/user-extensions/syntax-extensions.rst | 12 ++++++------
 1 file 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.
 
-- 
cgit v1.2.3