Scroll to navigation

COQIDE(1) General Commands Manual COQIDE(1)


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.
Add directory dir in the include path.
Recursively map physical dir to logical coqdir.
Add source directories in the include path.
Start with an empty state.
Load ML object file f.
Load ML file f.
Load Coq file f.v (Load f.).
Load Coq file f.v (Load Verbose f.).
Load Coq library path (Require path.).
Load Coq library path and import it (Require Import path.).
Compile Coq file f.v (implies -batch).
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.
Set the rcfile to f.
Tells Coq it is executed under Emacs.
Dump globalizations in file f (to be used by coqdoc(1)).
Set sort Set impredicative.
Don't load opaque proofs in memory.


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).