From 581bbbb23fcb488d5c1a10f360a6705a6792b2b1 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 14 Aug 2018 20:19:07 -0400
Subject: Add periods in response to PR comments

---
 doc/sphinx/user-extensions/syntax-extensions.rst | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc')

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
-- 
cgit v1.2.3