COQ(1)

NAME
coqmktop - The Coq user-tactics linker

SYNOPSIS
coqmktop [ ocamlmktop options ] [ -srcdir ] [ -notactics ] [ -o exec-file ] [ -opt ] [ -top ] [ -searchisos ] 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 must be called through coqtop(1), using the -image option.

OPTIONS

-srcdir directory
    Specify where the Coq source files are. The default is to search sources where Coq has been compiled.

-notactics
    High level tactics such as inversion tactics, Prolog, Tauto, etc. are included by default in the generated toplevel. This option specifies not to link these tactics.

-o exec-file
    Specify the name of the toplevel file produced by the linker. The default is coqcustom.out.

-opt
    Compile in native code.

-top
    Build Coq on top of a Caml toplevel.

-searchisos
    Build a toplevel for SearchIsos

The following options are forwarded to ocamlmktop / ocamlc / ocamlopt when linking the Objective Caml modules of Coq with the user objects: -I directory , -cclib library , -ccopt option , -compact , -linkall , -g . See ocamlmktop(1), ocamlc(1), ocamlopt(1) for information about these options.

SEE ALSO
coqtop(1), ocamlmktop(1). ocamlc(1). ocamlopt(1).
The Coq Reference Manual.