aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/user-extensions
diff options
context:
space:
mode:
authorJason Gross2018-08-14 20:19:07 -0400
committerJason Gross2018-08-31 20:05:54 -0400
commit581bbbb23fcb488d5c1a10f360a6705a6792b2b1 (patch)
treee0250040e842e1aaa68699a8ce1703195baeff22 /doc/sphinx/user-extensions
parent6a280b70fc66ff0231a9945cc3b3718385d3971c (diff)
Add periods in response to PR comments
Diffstat (limited to 'doc/sphinx/user-extensions')
-rw-r--r--doc/sphinx/user-extensions/syntax-extensions.rst6
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 2f7a7d42c1..6f655340da 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1443,19 +1443,19 @@ Numeral notations
The printing function given to the :cmd:`Numeral Notation`
vernacular is not of the right type.
- .. exn:: @type is not an inductive type
+ .. exn:: @type is not an inductive type.
Numeral notations can only be declared for inductive types with no
arguments.
- .. exn:: Unexpected term while parsing a numeral notation
+ .. 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.
- .. exn:: Unexpected non-option term while parsing a numeral notation
+ .. exn:: Unexpected non-option term @term while parsing a numeral notation.
Parsing functions expected to return an :g:`option` must always
return a concrete :g:`Some` or :g:`None` when applied to a