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