debian man page for coqmktop

COQ(1)							      General Commands Manual							    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

								  April 25, 2001							    COQ(1)