diff options
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 17 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 2 |
2 files changed, 12 insertions, 7 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 93dcfca4bf..ad1f0caa60 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -55,15 +55,20 @@ Customization at launch time By resource file ~~~~~~~~~~~~~~~~~~~~~~~ -When |Coq| is launched, with either ``coqtop`` or ``coqc``, the resource file -``$XDG_CONFIG_HOME/coq/coqrc.xxx`` is loaded, where ``$XDG_CONFIG_HOME`` +When |Coq| is launched, with either ``coqtop`` or ``coqc``, the +resource file ``$XDG_CONFIG_HOME/coq/coqrc.xxx``, if it exists, will +be implicitly prepended to any document read by Coq, whether it is an +interactive session or a file to compile. Here, ``$XDG_CONFIG_HOME`` is the configuration directory of the user (by default its home -directory ``/.config`` and ``xxx`` is the version number (e.g. 8.8). If +directory ``~/.config``) and ``xxx`` is the version number (e.g. 8.8). If this file is not found, then the file ``$XDG_CONFIG_HOME/coqrc`` is -searched. You can also specify an arbitrary name for the resource file +searched. If not found, it is the file ``~/.coqrc.xxx`` which is searched, +and, if still not found, the file ``~/.coqrc``. If the latter is also +absent, no resource file is loaded. +You can also specify an arbitrary name for the resource file (see option ``-init-file`` below). -This file may contain, for instance, ``Add LoadPath`` commands to add +The resource file may contain, for instance, ``Add LoadPath`` commands to add directories to the load path of |Coq|. It is possible to skip the loading of the resource file with the option ``-q``. @@ -171,7 +176,7 @@ and ``coqtop``, unless stated otherwise: Coq's auto-generated name scheme with names of the form *ident0*, *ident1*, etc. The command ``Set Mangle Names`` turns the behavior on in a document, and ``Set Mangle Names Prefix "ident"`` changes the used prefix. This feature - s intended to be used as a linter for developments that want to be robust to + is intended to be used as a linter for developments that want to be robust to changes in the auto-generated name scheme. The options are provided to facilitate tracking down problems. :-compat *version*: Attempt to maintain some backward-compatibility diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 59867988a4..59a88771a0 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -137,7 +137,7 @@ Here we describe only few of them. (e.g. wrappers) :COQ_SRC_SUBDIRS: can be extended by including other paths in which ``*.cm*`` files - are searched. For example ``COQ\_SRC\_SUBDIRS+=user-contrib/Unicoq`` + are searched. For example ``COQ_SRC_SUBDIRS+=user-contrib/Unicoq`` lets you build a plugin containing OCaml code that depends on the OCaml code of ``Unicoq``. |