man coqmktop (Commandes) - The Coq Proof Assistant user-tactics linker

NAME

coqmktop - The Coq Proof Assistant user-tactics linker

SYNOPSIS

coqmktop [ options ] files

DESCRIPTION

coqmktop builds a new Coq toplevel extended with user-tactics. files are the Objective Caml object or library files (i.e. with suffix .cmo, The linker produces an executable Coq toplevel which can be called directly or through coqc(1), using the -image option.

OPTIONS

-h
Help. List the available options.

SEE ALSO

coqtop(1), ocamlmktop(1). ocamlc(1). ocamlopt(1).

The Coq Reference Manual. The Coq web site: http://coq.inria.fr