COQ(1)

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, .cmx, .cma or .cmxa) to link with the Coq system. 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.

-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

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