Provided by: coqide_8.15.2+dfsg-2_amd64 bug


       coqide - The Coq Proof Assistant graphical interface


       coqide [ options ]


       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


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

              Set sort Set impredicative.

              Don't load opaque proofs in memory.


       coqc(1), coqtop(1), coq-tex(1), coqdep(1).
       The    Coq    Reference    Manual,    The    Coq    web     site:,


       This manual page was written by Samuel Mimram <>, for the Debian
       project (but may be used by others).