diff options
| author | Théo Zimmermann | 2020-10-19 16:06:30 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-10-20 11:07:52 +0200 |
| commit | 3230c568eb0bc719feca642a1537555e262478eb (patch) | |
| tree | 8d88af13db13ccf36fbe32826e711415c671e93a /doc/sphinx/using/tools | |
| parent | 7b07bc9aac0f7f990b8b12e7120d7a4e0bcd4fee (diff) | |
Add some missing smallcaps.
Diffstat (limited to 'doc/sphinx/using/tools')
| -rw-r--r-- | doc/sphinx/using/tools/coqdoc.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/using/tools/index.rst | 8 |
2 files changed, 7 insertions, 7 deletions
diff --git a/doc/sphinx/using/tools/coqdoc.rst b/doc/sphinx/using/tools/coqdoc.rst index 9ac3d2adda..88c1a575d9 100644 --- a/doc/sphinx/using/tools/coqdoc.rst +++ b/doc/sphinx/using/tools/coqdoc.rst @@ -253,7 +253,7 @@ The latter cannot be used around some inner parts of a proof, but can be used around a whole proof. Lastly, it is possible to adopt a middle-ground approach when the -desired output is HTML, where a given snippet of Coq material is +desired output is HTML, where a given snippet of |Coq| material is hidden by default, but can be made visible with user interaction. :: @@ -358,11 +358,11 @@ Command line options **Hyperlink options** :--glob-from file: Make references using |Coq| globalizations from file - file. (Such globalizations are obtained with Coq option ``-dump-glob``). + file. (Such globalizations are obtained with |Coq| option ``-dump-glob``). :--no-externals: Do not insert links to the |Coq| standard library. :--external url coqdir: Use given URL for linking references whose name starts with prefix ``coqdir``. - :--coqlib url: Set base URL for the Coq standard library (default is + :--coqlib url: Set base URL for the |Coq| standard library (default is `<http://coq.inria.fr/library/>`_). This is equivalent to ``--external url Coq``. :-R dir coqdir: Recursively map physical directory dir to |Coq| logical diff --git a/doc/sphinx/using/tools/index.rst b/doc/sphinx/using/tools/index.rst index dfe38dfce9..8543c5de8a 100644 --- a/doc/sphinx/using/tools/index.rst +++ b/doc/sphinx/using/tools/index.rst @@ -5,11 +5,11 @@ Command-line and graphical tools ================================ This chapter presents the command-line tools that users will need to -build their Coq project, the documentation of the CoqIDE standalone +build their |Coq| project, the documentation of the |CoqIDE| standalone user interface and the documentation of the parallel proof processing -feature that is supported by CoqIDE and several other user interfaces. -A list of available user interfaces to interact with Coq is available -on the `Coq website <https://coq.inria.fr/user-interfaces.html>`_. +feature that is supported by |CoqIDE| and several other user interfaces. +A list of available user interfaces to interact with |Coq| is available +on the `|Coq| website <https://coq.inria.fr/user-interfaces.html>`_. .. toctree:: :maxdepth: 1 |