11.3 Resource file
When Coq is launched, with either coqtop or coqc, the
resource file $HOME/.coqrc.7.0
is loaded, where $HOME
is
the home directory of the user. If this file is not found, then the
file $HOME/.coqrc
is searched. You can also specify an
arbitrary name for the resource file (see option -init-file
below), or the name of another user to load the resource file of
someone else (see option -user
).
This 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
.