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
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 <[email protected]>, for the Debian project (but may be used by others).