ROCQIDE(1) General Commands Manual ROCQIDE(1) NAME rocqide - graphical interface for the Rocq Prover SYNOPSIS rocqide [ options ] DESCRIPTION rocqide is a gtk graphical interface for the Rocq Prover. For command-line-oriented or batch-oriented use of Rocq, see rocq(1); OPTIONS -h Show the complete list of options accepted by rocqide. -I dir, -include dir Add directory dir in the include path. -R dir rocqdir Recursively map physical dir to logical rocqdir. -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 Rocq file f.v (Load f.). -lv f, -load-vernac-source-verbose f Load Rocq file f.v (Load Verbose f.). -load-vernac-object path Load Rocq library path (Require path.). -require-import path Load Rocq library path and import it (Require Import path.). -compile f Compile Rocq file f.v (implies -batch). -compile-verbose f Verbosely compile Rocq file f.v (implies -batch). -where Print Rocq's standard library location and exit. -v Print Rocq version and exit. -q Skip loading of rcfile. -init-file f Set the rcfile to f. -emacs Tells Rocq it is executed under Emacs. -dump-glob f Dump globalizations in file f (to be used by rocq(1)doc). -impredicative-set Set sort Set impredicative. -dont-load-proofs Don't load opaque proofs in memory. SEE ALSO rocq(1), The Rocq Reference Manual The Coq web site: http://coq.inria.fr /usr/share/doc/rocqide/FAQ AUTHOR This manual page was written by Samuel Mimram , for the Debian project (but may be used by others). ROCQIDE(1)