From a3869e5371c89629ddfd8ccdd1bdc0de12efe806 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 9 Nov 2020 18:39:49 +0100 Subject: [refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina. The smallcaps rendering was inexistent in the PDF version and did not look good in the HTML version. --- doc/sphinx/using/libraries/index.rst | 6 +++--- doc/sphinx/using/libraries/writing.rst | 8 ++++---- 2 files changed, 7 insertions(+), 7 deletions(-) (limited to 'doc/sphinx/using/libraries') diff --git a/doc/sphinx/using/libraries/index.rst b/doc/sphinx/using/libraries/index.rst index 95218322ff..0bd3054788 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 `_ and +the `Coq Package Index `_ and installed with the `opam package manager `_. diff --git a/doc/sphinx/using/libraries/writing.rst b/doc/sphinx/using/libraries/writing.rst index 724bcd0488..917edf0774 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 `_. Deprecating library objects or tactics -- cgit v1.2.3