FreeBSD Manual Pages
COQIDE(1) General Commands Manual COQIDE(1) NAME coqide - graphical interface for the Coq proof assistant 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-import 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). COQIDE(1)
NAME | SYNOPSIS | DESCRIPTION | OPTIONS | SEE ALSO | AUTHOR
Want to link to this manual page? Use this URL:
<https://man.freebsd.org/cgi/man.cgi?query=coqide&sektion=1&manpath=FreeBSD+Ports+15.1.quarterly>