Scroll to navigation

COQIDE(1) General Commands Manual COQIDE(1)

NAME

coqide - The Coq Proof Assistant graphical interface

SYNOPSIS

coqide [ options ]

DESCRIPTION

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

OPTIONS

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

SEE ALSO

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).
July 16, 2004