Man page - coqide(1)

Packages contains this manual

Package: coqide
apt-get install coqide

Manuals in package:

Documentations in package:

coqide

Manual

COQIDE

NAME
SYNOPSIS
DESCRIPTION
OPTIONS
SEE ALSO
AUTHOR

NAME

coqide - graphical interface for the Coq proof assistant

SYNOPSIS

coqide [ options ]

DESCRIPTION

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

-impredicative-set

Set sort Set impredicative.

-dont-load-proofs

Don’t load opaque proofs in memory.

AUTHOR

This manual page was written by Samuel Mimram <samuel.mimram@ens-lyon.org>, for the Debian project (but may be used by others).