1COQ(1)                      General Commands Manual                     COQ(1)
2
3
4

NAME

6       coqmktop - The Coq Proof Assistant user-tactics linker
7
8
9

SYNOPSIS

11       coqmktop [ options ] files
12
13
14

DESCRIPTION

16       coqmktop  builds  a new Coq toplevel extended with user-tactics.  files
17       are the Objective Caml object or library files (i.e. with suffix  .cmo,
18       .cmx,  .cma or .cmxa) to link with the Coq system.  The linker produces
19       an executable Coq toplevel which can  be  called  directly  or  through
20       coqc(1), using the -image option.
21
22

OPTIONS

24       -h     Help. List the available options.
25
26
27       -srcdir dir
28              Specify where the Coq source files are
29
30
31       -o exec-file
32              Specify the name of the resulting toplevel
33
34
35       -opt   Compile in native code
36
37
38       -full  Link high level tactics
39
40
41       -top   Build Coq on a ocaml toplevel (incompatible with -opt)
42
43
44       -searchisos
45              Build a toplevel for SearchIsos
46
47
48       -ide   Build a toplevel for the Coq IDE
49
50
51       -R dir Specify recursively directories for Ocaml
52
53
54       -v8    Link with V8 grammar
55
56
57

SEE ALSO

59       coqtop(1), ocamlmktop(1).  ocamlc(1).  ocamlopt(1).
60       The Coq Reference Manual.  The Coq web site: http://coq.inria.fr
61
62
63
64                                April 25, 2001                          COQ(1)