diff options
| author | Théo Zimmermann | 2020-04-28 10:20:37 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-04-28 10:20:37 +0200 |
| commit | 25c7e0cb30a7e196a293df9620bc4b801eaafa27 (patch) | |
| tree | 50d801f404aa55208e97a736f64e77edf08f2cda /doc/sphinx/practical-tools | |
| parent | d15b99d93b67f37a0c572950868713b2a7a2b1a4 (diff) | |
| parent | a7f56cb5799bc830285f4acf96678486a5929172 (diff) | |
Merge PR #11718: Convert syntax extensions chapter to prodn
Ack-by: JasonGross
Ack-by: Zimmi48
Ack-by: cpitclaudel
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/coqide.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index a045120b70..4e8a2b0879 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -206,7 +206,7 @@ Displaying Unicode symbols ~~~~~~~~~~~~~~~~~~~~~~~~~~ You just need to define suitable notations as described in the chapter -:ref:`syntaxextensionsandinterpretationscopes`. For example, to use the +:ref:`syntaxextensionsandnotationscopes`. For example, to use the mathematical symbols ∀ and ∃, you may define: .. coqtop:: in |