Merge PR #13329: [refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.

Reviewed-by: jfehrle
Reviewed-by: cpitclaudel

1 files changed, 23 insertions, 23 deletions

diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst
index 7a50748c51..e824ae152d 100644
--- a/doc/sphinx/addendum/parallel-proof-processing.rst
+++ b/doc/sphinx/addendum/parallel-proof-processing.rst
@@ -6,8 +6,8 @@ Asynchronous and Parallel Proof Processing
 :Author: Enrico Tassi
 
 This chapter explains how proofs can be asynchronously processed by
-|Coq|. This feature improves the reactivity of the system when used in
-interactive mode via |CoqIDE|. In addition, it allows |Coq| to take
+Coq. This feature improves the reactivity of the system when used in
+interactive mode via CoqIDE. In addition, it allows Coq to take
 advantage of parallel hardware when used as a batch compiler by
 decoupling the checking of statements and definitions from the
 construction and checking of proofs objects.
@@ -20,13 +20,13 @@ This feature has some technical limitations that may make it
 unsuitable for some use cases.
 
 For example, in interactive mode, some errors coming from the kernel
-of |Coq| are signaled late. The type of errors belonging to this
+of Coq are signaled late. The type of errors belonging to this
 category are universe inconsistencies.
 
 At the time of writing, only opaque proofs (ending with ``Qed`` or
 ``Admitted``) can be processed asynchronously.
 
-Finally, asynchronous processing is disabled when running |CoqIDE| in
+Finally, asynchronous processing is disabled when running CoqIDE in
 Windows. The current implementation of the feature is not stable on
 Windows. It can be enabled, as described below at :ref:`interactive-mode`,
 though doing so is not recommended.
@@ -34,12 +34,12 @@ though doing so is not recommended.
 Proof annotations
 ----------------------
 
-To process a proof asynchronously |Coq| needs to know the precise
+To process a proof asynchronously Coq needs to know the precise
 statement of the theorem without looking at the proof. This requires
 some annotations if the theorem is proved inside a Section (see
 Section :ref:`section-mechanism`).
 
-When a section ends, |Coq| looks at the proof object to decide which
+When a section ends, Coq looks at the proof object to decide which
 section variables are actually used and hence have to be quantified in
 the statement of the theorem. To avoid making the construction of
 proofs mandatory when ending a section, one can start each proof with
@@ -58,7 +58,7 @@ variables used.
 Automatic suggestion of proof annotations
 `````````````````````````````````````````
 
-The :flag:`Suggest Proof Using` flag makes |Coq| suggest, when a ``Qed``
+The :flag:`Suggest Proof Using` flag makes Coq suggest, when a ``Qed``
 command is processed, a correct proof annotation. It is up to the user
 to modify the proof script accordingly.
 
@@ -66,17 +66,17 @@ to modify the proof script accordingly.
 Proof blocks and error resilience
 --------------------------------------
 
-|Coq| 8.6 introduced a mechanism for error resilience: in interactive
-mode |Coq| is able to completely check a document containing errors
+Coq 8.6 introduced a mechanism for error resilience: in interactive
+mode Coq is able to completely check a document containing errors
 instead of bailing out at the first failure.
 
 Two kind of errors are supported: errors occurring in vernacular
 commands and errors occurring in proofs.
 
-To properly recover from a failing tactic, |Coq| needs to recognize the
+To properly recover from a failing tactic, Coq needs to recognize the
 structure of the proof in order to confine the error to a sub proof.
 Proof block detection is performed by looking at the syntax of the
-proof script (i.e. also looking at indentation). |Coq| comes with four
+proof script (i.e. also looking at indentation). Coq comes with four
 kind of proof blocks, and an ML API to add new ones.
 
 :curly: blocks are delimited by { and }, see Chapter :ref:`proofhandling`
@@ -92,13 +92,13 @@ Caveats
 When a vernacular command fails the subsequent error messages may be
 bogus, i.e. caused by the first error. Error resilience for vernacular
 commands can be switched off by passing ``-async-proofs-command-error-resilience off``
-to |CoqIDE|.
+to CoqIDE.
 
 An incorrect proof block detection can result into an incorrect error
 recovery and hence in bogus errors. Proof block detection cannot be
 precise for bullets or any other non well parenthesized proof
 structure. Error resilience can be turned off or selectively activated
-for any set of block kind passing to |CoqIDE| one of the following
+for any set of block kind passing to CoqIDE one of the following
 options:
 
 - ``-async-proofs-tactic-error-resilience off``
@@ -113,13 +113,13 @@ Interactive mode
 ---------------------
 
 At the time of writing the only user interface supporting asynchronous
-proof processing is |CoqIDE|.
+proof processing is CoqIDE.
 
-When |CoqIDE| is started, two |Coq| processes are created. The master one
+When CoqIDE is started, two Coq processes are created. The master one
 follows the user, giving feedback as soon as possible by skipping
 proofs, which are delegated to the worker process. The worker process,
 whose state can be seen by clicking on the button in the lower right
-corner of the main |CoqIDE| window, asynchronously processes the proofs.
+corner of the main CoqIDE window, asynchronously processes the proofs.
 If a proof contains an error, it is reported in red in the label of
 the very same button, that can also be used to see the list of errors
 and jump to the corresponding line.
@@ -137,14 +137,14 @@ Only then all the universe constraints are checked.
 Caveats
 ```````
 
-The number of worker processes can be increased by passing |CoqIDE|
+The number of worker processes can be increased by passing CoqIDE
 the ``-async-proofs-j n`` flag. Note that the memory consumption increases too,
 since each worker requires the same amount of memory as the master
 process. Also note that increasing the number of workers may reduce
 the reactivity of the master process to user commands.
 
 To disable this feature, one can pass the ``-async-proofs off`` flag to
-|CoqIDE|. Conversely, on Windows, where the feature is disabled by
+CoqIDE. Conversely, on Windows, where the feature is disabled by
 default, pass the ``-async-proofs on`` flag to enable it.
 
 Proofs that are known to take little time to process are not delegated
@@ -166,9 +166,9 @@ Batch mode
       a ``Require``. Indeed, the loading of a nonempty ``.vos`` file is
       assigned higher priority than the loading of a ``.vio`` file.
 
-When |Coq| is used as a batch compiler by running ``coqc``, it produces
+When Coq is used as a batch compiler by running ``coqc``, it produces
 a ``.vo`` file for each ``.v`` file. A ``.vo`` file contains, among other
-things, theorem statements and proofs. Hence to produce a .vo |Coq|
+things, theorem statements and proofs. Hence to produce a .vo Coq
 need to process all the proofs of the ``.v`` file.
 
 The asynchronous processing of proofs can decouple the generation of a
@@ -224,7 +224,7 @@ heavy use of the ``Type`` hierarchy.
 Limiting the number of parallel workers
 --------------------------------------------
 
-Many |Coq| processes may run on the same computer, and each of them may
+Many Coq processes may run on the same computer, and each of them may
 start many additional worker processes. The ``coqworkmgr`` utility lets
 one limit the number of workers, globally.
 
@@ -232,9 +232,9 @@ The utility accepts the ``-j`` argument to specify the maximum number of
 workers (defaults to 2). ``coqworkmgr`` automatically starts in the
 background and prints an environment variable assignment
 like ``COQWORKMGR_SOCKET=localhost:45634``. The user must set this variable
-in all the shells from which |Coq| processes will be started. If one
+in all the shells from which Coq processes will be started. If one
 uses just one terminal running the bash shell, then
 ``export ‘coqworkmgr -j 4‘`` will do the job.
 
-After that, all |Coq| processes, e.g. ``coqide`` and ``coqc``, will respect the
+After that, all Coq processes, e.g. ``coqide`` and ``coqc``, will respect the
 limit, globally.