blob: 0535e6e29ee5302592749e63325678db6ee9988c (
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
|
.TH COQ 1 "April 25, 2001"
.SH NAME
coqc \- The Coq Proof Assistant compiler
.SH SYNOPSIS
.B coqc
[
.B general \ Coq \ options
]
.I file
.SH DESCRIPTION
.B coqc
is the batch compiler for the Coq Proof Assistant.
The options are basically the same as coqtop(1).
.IR file.v \&
is the vernacular file to compile.
.IR file \&
must be formed
only with the characters `a` to `Z`, `0`-`9` or `_` and must begin
with a letter.
The compiler produces an object file
.IR file.vo \&.
For interactive use of Coq, see
.BR coqtop(1).
.SH OPTIONS
.TP
.BI \-h
Will give you a description of the whole list of options of coqc and
coqtop.
.SH SEE ALSO
.BR coqtop (1),
.BR coqdep (1).
.br
.I
The Coq Reference Manual.
.I
The Coq web site: http://coq.inria.fr
|
