coqide - The Coq Proof Assistant graphical interface
coqide [ options ]
coqtop is a gtk graphical interface for the Coq proof assistant.
For command-line-oriented use of Coq, see coqide(1) ; for batch-
oriented use of Coq, see coqc(1).
-h 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.
-src Add source directories in the include path.
-is f, -inputstate f
Read state from f.coq.
-nois Start with an empty state.
Write state in file f.coq.
Load ML object file 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 Coq object file f.vo.
Load Coq object file f.vo and import it (Require f.).
Compile Coq file f.v (implies -batch).
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.
Set the rcfile to f.
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 globalizations in file f (to be used by coqdoc(1)).
Set sort Set impredicative.
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).
coqc(1), coqtop(1), coq-tex(1), coqdep(1).
The Coq Reference Manual, The Coq web site: http://coq.inria.fr,
This manual page was written by Samuel Mimram <samuel.mimram@ens-
lyon.org>, for the Debian project (but may be used by others).
July 16, 2004