diff options
| author | Matthieu Sozeau | 2018-10-29 16:07:28 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-10-30 20:23:09 +0100 |
| commit | 4f4d2a68c58f2e54f0eafc8bc152f2d378eacefd (patch) | |
| tree | de5bef18806b2fcf41605f8fc867f36f8c0144b0 /doc/sphinx/user-extensions | |
| parent | 0ac673e562c34245e4e48efc428d808e917be79b (diff) | |
Credits for 8.9
Adressed comments by Guillaume and Jason
Updated according to Zimmi48's input.
Better link to custom entries
Fix typesetting
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. |