11.3 Resource file

When Coq is launched, with either coqtop or coqc, the resource file $HOME/.coqrc.6.2.4 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 variable $COQLIB which refer to the Coq library. Remember that the default load path already contains the following directories:

           .
           $CAMLP4LIB
           $COQLIB/tactics/tcc
           $COQLIB/tactics/programs/EXAMPLES
           $COQLIB/tactics/programs
           $COQLIB/tactics/contrib/polynom
           $COQLIB/tactics/contrib/omega
           $COQLIB/tactics/contrib/natural
           $COQLIB/tactics/contrib/linear
           $COQLIB/tactics/contrib/extraction
           $COQLIB/tactics/contrib/acdsimpl/simplify_rings
           $COQLIB/tactics/contrib/acdsimpl/simplify_naturals
           $COQLIB/tactics/contrib/acdsimpl/acd_simpl_def
           $COQLIB/tactics/contrib/acdsimpl
           $COQLIB/tactics/contrib
           $COQLIB/theories/ZARITH
           $COQLIB/theories/TREES
           $COQLIB/theories/TESTS
           $COQLIB/theories/SORTING
           $COQLIB/theories/SETS
           $COQLIB/theories/RELATIONS/WELLFOUNDED
           $COQLIB/theories/RELATIONS
           $COQLIB/theories/LOGIC
           $COQLIB/theories/LISTS
           $COQLIB/theories/INIT
           $COQLIB/theories/DEMOS/PROGRAMS
           $COQLIB/theories/DEMOS/OMEGA
           $COQLIB/theories/DEMOS
           $COQLIB/theories/BOOL
           $COQLIB/theories/REALS
           $COQLIB/theories/ARITH
           $COQLIB/tactics
           $COQLIB/states

It is possible to skip the loading of the resource file with the option -q.