diff options
| author | Guillaume Melquiond | 2018-10-31 09:40:48 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2018-10-31 09:40:48 +0100 |
| commit | 310f8fa900bc0d25a05f6409d941708a74aca60b (patch) | |
| tree | ed9f9330a604b53c2234a9105e3d92654a893b14 /doc/sphinx/user-extensions | |
| parent | 20752cb329262ddb4b4a9ba898fd8566bf5ad156 (diff) | |
| parent | 4f4d2a68c58f2e54f0eafc8bc152f2d378eacefd (diff) | |
Merge PR #8851: Credits for 8.9
Diffstat (limited to 'doc/sphinx/user-extensions')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 705d67e6c6..2214cbfb34 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -692,6 +692,8 @@ side. E.g.: Notation "'apply_id' f a1 .. an" := (.. (f a1) .. an) (at level 10, f ident, a1, an at level 9). +.. _custom-entries: + Custom entries ~~~~~~~~~~~~~~ @@ -1372,11 +1374,11 @@ Abbreviations denoted expression is performed at definition time. Type checking is done only at the time of use of the abbreviation. - Numeral notations ----------------- .. cmd:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope. + :name: Numeral Notation This command allows the user to customize the way numeral literals are parsed and printed. |