diff options
| author | Vincent Laporte | 2019-10-31 15:39:52 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-10-31 15:39:52 +0000 |
| commit | 73817b93eb604c680e661c0064af2e916c6ffe69 (patch) | |
| tree | a558acf41fd01b976c2eff2c2b3c836618dac7dc /doc/sphinx | |
| parent | a1ea0da415df9137576ea60af5f68ae25dfad1b9 (diff) | |
| parent | cd7e8284c7defdad636ffa7ef87f3e584a7592fb (diff) | |
Merge PR #9883: Add support for Sorts in numeral notations
Ack-by: SkySkimmer
Ack-by: proux01
Reviewed-by: vbgl
Diffstat (limited to 'doc/sphinx')
| -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 |