coqide man page

coqide — The Coq Proof Assistant graphical interface


coqide [ options ]


coqide is a gtk graphical interface for the Coq proof assistant.

For command-line-oriented use of Coq, see coqtop(1) ; for batch-oriented use of Coq, see coqc(1).



Show the complete list of options accepted by coqide.

-I dir-include dir

Add directory dir in the include path.

-R dir coqdir

Recursively map physical dir to logical coqdir.


Add source directories in the include path.


Start with an empty state.

-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 path

Load Coq library path (Require path.).

-require path

Load Coq library path and import it (Require Import path.).

-compile f

Compile Coq file f.v (implies -batch).

-compile-verbose f

Verbosely compile Coq file f.v (implies -batch).


Print Coq's standard library location and exit.


Print Coq version and exit.


Skip loading of rcfile.

-init-file f

Set the rcfile to f.


Batch mode (exits just after arguments parsing).


Boot mode (implies -q and -batch).


Tells Coq it is executed under Emacs.

-dump-glob f

Dump globalizations in file f (to be used by coqdoc(1)).


Set sort Set impredicative.


Don't load opaque proofs in memory.


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), coqtop(1), coq-tex(1), coqdep(1).
The Coq Reference Manual, The Coq web site:, /usr/share/doc/coqide/FAQ.


This manual page was written by Samuel Mimram <>, for the Debian project (but may be used by others).


July 16, 2004