blob: 1b9c9e2a18c4ed7559bd5e168b905fe8f30e1bf8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
|
.TH COQ 1 "April 25, 2001"
.SH NAME
coqmktop \- The Coq Proof Assistant user-tactics linker
.SH SYNOPSIS
.B coqmktop
[
.I options
]
.I files
.SH DESCRIPTION
.B coqmktop
builds a new Coq toplevel extended with user-tactics.
.IR 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.
.SH OPTIONS
.TP
.BI \-h
Help. List the available options.
.TP
.BI \-srcdir \ dir
Specify where the Coq source files are
.TP
.BI \-o \ exec\-file
Specify the name of the resulting toplevel
.TP
.B \-opt
Compile in native code
.TP
.B \-full
Link high level tactics
.TP
.B \-top
Build Coq on a ocaml toplevel (incompatible with
.BR \-opt )
.TP
.B \-searchisos
Build a toplevel for SearchIsos
.TP
.B \-ide
Build a toplevel for the Coq IDE
.TP
.BI \-R \ dir
Specify recursively directories for Ocaml
.TP
.B \-v8
Link with V8 grammar
.SH SEE ALSO
.BR coqtop (1),
.BR ocamlmktop (1).
.BR ocamlc (1).
.BR ocamlopt (1).
.br
.I
The Coq Reference Manual.
.I
The Coq web site: http://coq.inria.fr
|
