aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Lysxia <lysxia@gmail.com>2018-06-29 15:57:46 -0400
committerGravatar Lysxia <lysxia@gmail.com>2018-06-29 16:43:28 -0400
commit905770ed2a8b9b760b9a8c1384d4d65cdb82892e (patch)
tree2f553cb70d3f477ab6c504d1e0617feaf9ed2090 /doc
parente25d69f5d47f7ad6584bf54ea48e42fd482c95e0 (diff)
doc: Fix typesetting in Gallina extensions
Diffstat (limited to 'doc')
-rw-r--r--doc/sphinx/language/gallina-extensions.rst14
1 files changed, 7 insertions, 7 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 8fbd2ea4e..509ac92f8 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1349,7 +1349,7 @@ folder ``path/fOO/Bar`` maps to ``Lib.fOO.Bar``. Subdirectories corresponding
to invalid |Coq| identifiers are skipped, and, by convention,
subdirectories named ``CVS`` or ``_darcs`` are skipped too.
-Thanks to this mechanism, .vo files are made available through the
+Thanks to this mechanism, ``.vo`` files are made available through the
logical name of the folder they are in, extended with their own
basename. For example, the name associated to the file
``path/fOO/Bar/File.vo`` is ``Lib.fOO.Bar.File``. The same caveat applies for
@@ -1360,17 +1360,17 @@ wrong loadpath afterwards.
Some folders have a special status and are automatically put in the
path. |Coq| commands associate automatically a logical path to files in
the repository trees rooted at the directory from where the command is
-launched, coqlib/user-contrib/, the directories listed in the
-`$COQPATH`, `${XDG_DATA_HOME}/coq/` and `${XDG_DATA_DIRS}/coq/`
-environment variables (see`http://standards.freedesktop.org/basedir-
-spec/basedir-spec-latest.html`_) with the same physical-to-logical
-translation and with an empty logical prefix.
+launched, ``coqlib/user-contrib/``, the directories listed in the
+``$COQPATH``, ``${XDG_DATA_HOME}/coq/`` and ``${XDG_DATA_DIRS}/coq/``
+environment variables (see `XDG base directory specification
+<http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html>`_)
+with the same physical-to-logical translation and with an empty logical prefix.
The command line option ``-R`` is a variant of ``-Q`` which has the strictly
same behavior regarding loadpaths, but which also makes the
corresponding ``.vo`` files available through their short names in a way
not unlike the ``Import`` command (see :ref:`here <import_qualid>`). For instance, ``-R`` `path` ``Lib``
-associates to the ``filepath/fOO/Bar/File.vo`` the logical name
+associates to the file path `path`\ ``/path/fOO/Bar/File.vo`` the logical name
``Lib.fOO.Bar.File``, but allows this file to be accessed through the
short names ``fOO.Bar.File,Bar.File`` and ``File``. If several files with
identical base name are present in different subdirectories of a