COQIDE(1)						      General Commands Manual							 COQIDE(1)

NAME

       coqide - The Coq Proof Assistant graphical interface

SYNOPSIS

       coqide [ options ]

DESCRIPTION

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

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.

       -is f, -inputstate f
	      Read state from f.coq.

       -nois  Start with an empty state.

       -outputstate f
	      Write state in file f.coq.

       -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 f
	      Load Coq object file f.vo.

       -require f
	      Load Coq object file f.vo and import it (Require f.).

       -compile f
	      Compile Coq file f.v (implies -batch).

       -compile-verbose f
	      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.

       -init-file f
	      Set the rcfile to f.

       -user u
	      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-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.

       -xml   Export XML files either to the hierarchy rooted in the directory COQ_XML_LIBRARY_ROOT (if set) or to stdout (if unset).

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							 COQIDE(1)