diff options
| author | coqbot-app[bot] | 2020-09-14 04:09:01 +0000 |
|---|---|---|
| committer | GitHub | 2020-09-14 04:09:01 +0000 |
| commit | 9278a6ec5b0cc33691b441beaa73cf38f04f4cbb (patch) | |
| tree | a227ceaf8facc226ee39a10bd18a7d8fa06ec4c2 /doc | |
| parent | e0696ef1db06dbe32c95ac16b9c54d6b3624dff0 (diff) | |
| parent | d7d41bee6ae195a7842c40d84162eb1e26a24533 (diff) | |
Merge PR #13022: Fixing documentation relatively to example of use of extra spaces in notations
Reviewed-by: jfehrle
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 838705e100..6ba53b581b 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -241,12 +241,12 @@ notation is the insertion of spaces at some places of the notation. This is performed by adding extra spaces between the symbols and parameters: each extra space (other than the single space needed to separate the components) is interpreted as a space to be inserted by -the printer. Here is an example showing how to add spaces around the -bar of the notation. +the printer. Here is an example showing how to add spaces next to the +curly braces. .. coqtop:: in - Notation "{{ x : A | P }}" := (sig (fun x : A => P)) (at level 0, x at level 99). + Notation "{{ x : A | P }}" := (sig (fun x : A => P)) (at level 0, x at level 99). .. coqtop:: all |