From 73c924d3d4bcc22a179cb974603f9072599ebb77 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sun, 31 Mar 2019 15:35:21 -0400
Subject: Update numeral notation printing doc

Fixes #9844
---
 doc/sphinx/user-extensions/syntax-extensions.rst | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'doc/sphinx')

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index e5eb7eb4f5..1e201953b3 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1473,6 +1473,10 @@ Numeral notations
      :n:`@ident__2` to the number will be fully reduced, and universes
      of the resulting term will be refreshed.
 
+     Note that only fully-reduced ground terms (terms containing only
+     function application, constructors, inductive type families, and
+     primitive integers) will be considered for printing.
+
    .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num).
 
      When a literal larger than :token:`num` is parsed, a warning
@@ -1618,6 +1622,10 @@ String notations
      :n:`@ident__2` to the string will be fully reduced, and universes
      of the resulting term will be refreshed.
 
+     Note that only fully-reduced ground terms (terms containing only
+     function application, constructors, inductive type families, and
+     primitive integers) will be considered for printing.
+
    .. exn:: Cannot interpret this string as a value of type @type
 
      The string notation registered for :token:`type` does not support
-- 
cgit v1.2.3