Provided by: coq_8.1.pl3+dfsg-1_i386 bug

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.

       -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

                                April 25, 2001                          COQ(1)