| COQIDE(1) | General Commands Manual | COQIDE(1) |
NAME¶
coqide - graphical interface for the Coq proof assistant
SYNOPSIS¶
coqide[options]
DESCRIPTION¶
coqideis a gtk graphical interface for the Coq proof assistant.
For command-line-oriented use of Coq, seecoqtop(1);for batch-oriented use of Coq, seecoqc(1).
OPTIONS¶
- -h
- Show the complete list of options accepted bycoqide.
- -I dir, -include dir
- Add directorydirin the include path.
- -R dir coqdir
- Recursively map physicaldirto logicalcoqdir.
- -src
- Add source directories in the include path.
- -nois
- Start with an empty state.
- -load-ml-object f
- Load ML object filef.
- -load-ml-source f
- Load ML filef.
- -l f, -load-vernac-source f
- Load Coq filef.v(Loadf.).
- -lv f, -load-vernac-source-verbose f
- Load Coq filef.v(Load Verbosef.).
- -load-vernac-object path
- Load Coq librarypath(Requirepath.).
- -require-import path
- Load Coq librarypathand import it (Require Importpath.).
- -compile f
- Compile Coq filef.v(implies-batch).
- -compile-verbose f
- Verbosely compile Coq filef.v(implies-batch).
- -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 tof.
- -emacs
- Tells Coq it is executed under Emacs.
- -dump-glob f
- Dump globalizations in filef(to be used bycoqdoc(1)).
- -impredicative-set
- Set sort Set impredicative.
- -dont-load-proofs
- Don't load opaque proofs in memory.
SEEALSO¶
coqc(1),coqtop(1),coq-tex(1),coqdep(1)
The Coq Reference Manual
The Coq web site: http://coq.inria.fr
/usr/share/doc/coqide/FAQ
AUTHOR¶
This manual page was written by Samuel Mimram <samuel.mimram@ens-lyon.org>,for the Debian project (but may be used by others).