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)

       -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

                                          April 25, 2001                                   COQ(1)