man coq-interface.opt (Commandes) - coq-interface -

NAME

coq-interface -

SYNOPSIS

coq-interface [ options ]

DESCRIPTION

coq-interface is a Coq customized toplevel system for Coq containing some modules useful for the graphical interface. This program is not for the casual user.

OPTIONS

-h
Help. Will give you the complete list of options accepted by coq-interface (the same as coqtop). -I dir, -include dir Add directory dir in the include path.
-R dir coqdir
Recursively map physical dir to logical coqdir.
-src
Add source directories in the include path.
-is f, -inputstate f
Read state from f.coq.
-nois
Start with an empty state.
-outputstate f
Write state in file f.coq.
-load-ml-object f
Load ML object file f.
-load-ml-source f
Load ML file f.
-l f, -load-vernac-source f
Load Coq file f.v (Load f.).
-lv f, -load-vernac-source-verbose f
Load Coq file f.v (Load Verbose f.).
-load-vernac-object f
Load Coq object file f.vo.
-require f
Load Coq object file f.vo and import it (Require f.).
-compile f
Compile Coq file f.v (implies -batch).
-compile-verbose f
Verbosely compile Coq file f.v (implies -batch).
-opt
Run the native-code version of Coq or Coq_SearchIsos.
-byte
Run the bytecode version of Coq or Coq_SearchIsos.
-where
Print Coq's standard library location and exit.
-v
Print Coq version and exit.
-q
Skip loading of rcfile.
-init-file f
Set the rcfile to f.
-user u
Use the rcfile of user u.
-batch
Batch mode (exits just after arguments parsing).
-boot
Boot mode (implies -q and -batch).
-emacs
Tells Coq it is executed under Emacs.
-dump-glob f
Dump globalizations in file f (to be used by coqdoc(1)).
-impredicative-set
Set sort Set impredicative.
-dont-load-proofs
Don't load opaque proofs in memory.
-xml
Export XML files either to the hierarchy rooted in the directory COQ_XML_LIBRARY_ROOT (if set) or to stdout (if unset).

SEE ALSO

coqc(1), coqdep(1), coqtop(1), parser(1).

The Coq Reference Manual. The Coq web site: http://coq.inria.fr