diff options
| author | Jim Fehrle | 2020-02-29 12:27:51 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2020-04-26 22:19:01 -0700 |
| commit | a7f56cb5799bc830285f4acf96678486a5929172 (patch) | |
| tree | 12c83204413ad08255400b3e35c508e6815cd9c0 /doc/sphinx/practical-tools | |
| parent | 51a938a260d989f11fb1cd1d7a0205c6183f3809 (diff) | |
Convert syntax extensions chapter to prodn
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 a69521c278..0f255e4e64 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -219,7 +219,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 |