Man pages sections > man1 > coqmktop

coqmktop - The Coq Proof Assistant user-tactics linker

COQ(1) General Commands Manual COQ(1)


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.


Help. List the available options.
-srcdir dir
Specify where the Coq source files are
-o exec-file
Specify the name of the resulting toplevel
Compile in native code
Link high level tactics
Build Coq on a ocaml toplevel (incompatible with -opt)
-R dir
Specify recursively directories for Ocaml
Link with V8 grammar


coqtop(1), ocamlmktop(1). ocamlc(1). ocamlopt(1).
The Coq Reference Manual. The Coq web site:
April 25, 2001 Debian Sid