diff options
| author | coqbot-app[bot] | 2020-10-22 20:32:00 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-22 20:32:00 +0000 |
| commit | 00b82b7399ce01730371b8e80315f65e9254da91 (patch) | |
| tree | ba146f40a345d99ef476d2e85151b08c640edfc0 /doc/sphinx/using/libraries | |
| parent | fe095cd8b63e363e82953503cb84a851296c1965 (diff) | |
| parent | 3230c568eb0bc719feca642a1537555e262478eb (diff) | |
Merge PR #11924: Add style for smallcaps.
Reviewed-by: jfehrle
Diffstat (limited to 'doc/sphinx/using/libraries')
| -rw-r--r-- | doc/sphinx/using/libraries/index.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/using/libraries/writing.rst | 10 |
2 files changed, 8 insertions, 8 deletions
diff --git a/doc/sphinx/using/libraries/index.rst b/doc/sphinx/using/libraries/index.rst index 0bd3054788..95218322ff 100644 --- a/doc/sphinx/using/libraries/index.rst +++ b/doc/sphinx/using/libraries/index.rst @@ -4,15 +4,15 @@ Libraries and plugins ===================== -Coq is distributed with a standard library and a set of internal +|Coq| is distributed with a standard library and a set of internal plugins (most of which provide tactics that have already been presented in :ref:`writing-proofs`). This chapter presents this standard library and some of these internal plugins which provide features that are not tactics. -In addition, Coq has a rich ecosystem of external libraries and +In addition, |Coq| has a rich ecosystem of external libraries and plugins. These libraries and plugins can be browsed online through -the `Coq Package Index <https://coq.inria.fr/opam/www/>`_ and +the `|Coq| Package Index <https://coq.inria.fr/opam/www/>`_ and installed with the `opam package manager <https://coq.inria.fr/opam-using.html>`_. diff --git a/doc/sphinx/using/libraries/writing.rst b/doc/sphinx/using/libraries/writing.rst index 325ea2af60..724bcd0488 100644 --- a/doc/sphinx/using/libraries/writing.rst +++ b/doc/sphinx/using/libraries/writing.rst @@ -1,9 +1,9 @@ -Writing Coq libraries and plugins -================================= +Writing |Coq| libraries and plugins +=================================== -This section presents the part of the Coq language that is useful only -to library and plugin authors. A tutorial for writing Coq plugins is -available in the Coq repository in `doc/plugin_tutorial +This section presents the part of the |Coq| language that is useful only +to library and plugin authors. A tutorial for writing |Coq| plugins is +available in the |Coq| repository in `doc/plugin_tutorial <https://github.com/coq/coq/tree/master/doc/plugin_tutorial>`_. Deprecating library objects or tactics |