diff options
| author | Hugo Herbelin | 2019-11-12 22:09:07 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-19 21:09:07 +0100 |
| commit | 8364b7fea91a11ad07d94057f3a5a938b9524d81 (patch) | |
| tree | 016e7702619652adc06af93ab3c1dff1c2558ac5 /doc | |
| parent | 039b2423cf7b85f2f5960dde6a1586f0f07cf9d0 (diff) | |
Short allusion in refman on the existence of a generic and specific format.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 04419f08f7..7c628e534b 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -354,6 +354,11 @@ Reserving notations This command declares an infix parsing rule without giving its interpretation. + When a format is attached to a reserved notation, it is used by + default by all subsequent interpretations of the corresponding + notation. A specific interpretation can provide its own format + overriding the default format though. + Simultaneous definition of terms and notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |