Man Linux: Main Page and Category List


       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,
       .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.


       -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)

              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:

                                April 25, 2001