Man Linux: Main Page and Category List

coqide - The Coq Proof Assistant graphical interface

coqide[options]

coqtopis a gtk graphical interface for the Coq proof assistant. For command-line-oriented use of Coq, seecoqide(1) ; for batch- oriented use of Coq, seecoqc(1).

-hShow the complete list of options accepted bycoqide.-Idir,-includedirAdd directory dir in the include path.-RdircoqdirRecursively map physicaldirto logicalcoqdir.-srcAdd source directories in the include path.-isf,-inputstatefRead state fromf.coq.-noisStart with an empty state.-outputstatefWrite state in filef.coq.-load-ml-objectfLoad ML object filef.-load-ml-sourcefLoad ML filef.-lf,-load-vernac-sourcefLoad Coq filef.v (Loadf.).-lvf,-load-vernac-source-verbosefLoad Coq filef.v (Load Verbosef.).-load-vernac-objectfLoad Coq object filef.vo.-requirefLoad Coq object filef.vo and import it (Requiref.).-compilefCompile Coq filef.v (implies-batch).-compile-verbosefVerbosely compile Coq filef.v (implies-batch).-optRun the native-code version of Coq or Coq_SearchIsos.-byteRun the bytecode version of Coq or Coq_SearchIsos.-wherePrint Coq's standard library location and exit.-vPrint Coq version and exit.-qSkip loading of rcfile.-init-filefSet the rcfile tof.-useruUse the rcfile of useru.-batchBatch mode (exits just after arguments parsing).-bootBoot mode (implies-qand-batch).-emacsTells Coq it is executed under Emacs.-dump-globfDump globalizations in filef(to be used bycoqdoc(1)).-impredicative-setSet sort Set impredicative.-dont-load-proofsDon't load opaque proofs in memory.-xmlExport XML files either to the hierarchy rooted in the directoryCOQ_XML_LIBRARY_ROOT(if set) or to stdout (if unset).

coqc(1),coqtop(1),coq-tex(1),coqdep(1).TheCoqReferenceManual,TheCoqwebsite:http://coq.inria.fr,/usr/share/doc/coqide/FAQ.

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