11.5 Options

-opt

Run the native-code version of Coq (or Coq_SearchIsos for coqtop).

-full

Run a native-code version of Coq with all tactics.

-I directory, -include directory

Add directory to the searched directories when looking for a file.

-R directory

Add recursively directory to the searched directories when looking for a file.

-is file, -inputstate file

Cause Coq to use the state put in the file file as its input state. The default state is tactics.coq. Mainly useful to build the standard input state.

-nois

Cause Coq to begin with an empty state. Mainly useful to build the standard input state.

-notactics

Forbid the dynamic loading of tactics, and start on the input state state.coq.

-init-file file

Take file as resource file, instead of $HOME/.coqrc.6.2.4.

-q

Cause Coq not to load the resource file.

-user username

Take resource file of user username (that is ~username/.coqrc.6.2.4) instead of yours.

-load-ml-source file

Load the Caml source file file.

-load-ml-object file

Load the Caml object file file.

-load-vernac-source file

Load Coq file file.v

-load-vernac-object file

Load Coq compiled file file.vo

-require file

Load Coq compiled file file.vo and import it (Require file).

-batch

Batch mode : exit just after arguments parsing. This option is only used by coqc.

-debug

Switch on the debug flag.

-emacs

Tells Coq it is executed under Emacs.

-db

Launch Coq under the Objective Caml debugger (provided that Coq has been compiled for debugging; see next chapter).

-image file

This option sets the binary image to be used to be file instead of the standard one. Not of general use.

-bindir directory

It is equivalent to do export COQBIN=directory before lauching Coq.

-libdir file

It is equivalent to do export COQLIB=directory before lauching Coq.

-where

Print the Coq's standard library location and exit.

-v

Print the Coq's version and exit.

-h, --help

Print a short usage and exit.

-searchisos

Launch the Coq_SearchIsos toplevel (see section 12.4, page X).