11.3 Resource file
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
.
Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.3.0.2.html at 8/10/98