Add support for Sorts in numeral notations

2 files changed, 8 insertions, 4 deletions

diff --git a/doc/changelog/03-notations/09883-numeral-notations-sorts.rst b/doc/changelog/03-notations/09883-numeral-notations-sorts.rst
new file mode 100644
index 0000000000..abc5a516ae
--- /dev/null
+++ b/doc/changelog/03-notations/09883-numeral-notations-sorts.rst
@@ -0,0 +1,4 @@
+- Numeral Notations now support sorts in the input to printing
+  functions (e.g., numeral notations can be defined for terms
+  containing things like `@cons Set nat nil`).  (`#9883
+  <https://github.com/coq/coq/pull/9883>`_, by Jason Gross).
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index a28ce600ca..02910e603a 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1442,8 +1442,8 @@ Numeral notations
      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.
+     function application, constructors, inductive type families,
+     sorts, and primitive integers) will be considered for printing.
 
    .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num).
 
@@ -1592,8 +1592,8 @@ String notations
      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.
+     function application, constructors, inductive type families,
+     sorts, and primitive integers) will be considered for printing.
 
    .. exn:: Cannot interpret this string as a value of type @type