diff options
Diffstat (limited to 'doc/sphinx/README.rst')
| -rw-r--r-- | doc/sphinx/README.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 4461ff9240..bfdbc4c4db 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -551,7 +551,7 @@ Add either ``abort`` to the first block or ``reset`` to the second block to avoi Abbreviations and macros ------------------------ -Substitutions for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``), along with some useful LaTeX macros, are defined in a `separate file </doc/sphinx/refman-preamble.rst>`_. This file is automatically included in all manual pages. +Substitutions for specially-formatted names (like ``|Cic|``, ``|Ltac|`` and ``|Latex|``), along with some useful LaTeX macros, are defined in a `separate file </doc/sphinx/refman-preamble.rst>`_. This file is automatically included in all manual pages. Emacs ----- |