diff options
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 12 |
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. |