diff options
Diffstat (limited to 'doc/sphinx/user-extensions')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 8 |
1 files changed, 4 insertions, 4 deletions
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 |