11.3 Resource file
When Coq is launched, with either coqtop or coqc, the resource file$HOME/.coqrc.6.2 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,
AddPath commands to add
directories to the load path of Coq. You can use the environment
variables $COQLIB and $COQTH which refer to the Coq library and its subdirectory theories. Remember that the
default load path already contains the following directories:
.
$COQLIB/tactics/contrib/polynom
$COQLIB/tactics/contrib/omega
$COQLIB/tactics/contrib/natural
$COQLIB/tactics/contrib/extraction
$COQLIB/tactics/contrib/linear
$COQLIB/tactics
$COQLIB/theories/SORTING
$COQLIB/theories/ZARITH
$COQLIB/theories/ARITH
$COQLIB/theories/RELATIONS/WELLFOUNDED
$COQLIB/theories/RELATIONS
$COQLIB/theories/LOGIC
$COQLIB/theories/SETS
$COQLIB/theories/BOOL
$COQLIB/theories/LISTS
$COQLIB/theories/INIT
$COQLIB/states
It is possible to skip the loading of the resource file with the option
-q.