blob: 05e73d759ab8a63e03f46d7a679bf4f1871cbb91 (
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
|
.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.
.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
|
