COQ

coqmktop − The Coq Proof Assistant user-tactics linker

coqmktop [ options ] files

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.

−h

Help. List the available options.

−srcdir dir

Specify where the Coq source files are

−o exec−file

Specify the name of the resulting toplevel

−opt

Compile in native code

−full

Link high level tactics

−top

Build Coq on a ocaml toplevel (incompatible with −opt)

−searchisos

Build a toplevel for SearchIsos

−ide

Build a toplevel for the Coq IDE

−R dir

Specify recursively directories for Ocaml

−v8

Link with V8 grammar

coqtop(1), ocamlmktop(1). ocamlc(1). ocamlopt(1).
The Coq Reference Manual. The Coq web site: http://coq.inria.fr