diff options
| author | Théo Zimmermann | 2019-10-24 10:15:08 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-10-24 10:15:08 +0200 |
| commit | 2d8371ffe5b7fb1fa0a6f7b647415243802cbb8f (patch) | |
| tree | ba6b508040ad181b7e712434f5653610b9806d7b /doc/sphinx/user-extensions | |
| parent | e6991dce306c41352c359a8ba5d6d9d6c5e6dfb2 (diff) | |
| parent | cc2e8fedc55a267d9d5a23015c173b1402e964a5 (diff) | |
Merge PR #10938: Better wording for "Show Proof" and fix typos
Reviewed-by: Zimmi48
Diffstat (limited to 'doc/sphinx/user-extensions')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index bcc5e914ac..a28ce600ca 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -750,12 +750,12 @@ level is otherwise given explicitly by using the syntax Levels are cumulative: a notation at level ``n`` of which the left end is a term shall use rules at level less than ``n`` to parse this -sub-term. More precisely, it shall use rules at level strictly less +subterm. More precisely, it shall use rules at level strictly less than ``n`` if the rule is declared with ``right associativity`` and rules at level less or equal than ``n`` if the rule is declared with ``left associativity``. Similarly, a notation at level ``n`` of which the right end is a term shall use by default rules at level strictly -less than ``n`` to parse this sub-term if the rule is declared left +less than ``n`` to parse this subterm if the rule is declared left associative and rules at level less or equal than ``n`` if the rule is declared right associative. This is what happens for instance in the rule |