aboutsummaryrefslogtreecommitdiffhomepage
path: root/man/coq-parser.1
blob: 23dc8201930ff1a57c33faed6842ddfa42aead30 (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
.TH COQ 1 "April 25, 2001"

.SH NAME
coq\-parser \- Coq parser


.SH SYNOPSIS
.B coq\-parser
[
.B options
]

.SH DESCRIPTION

.B parser
is a program reading Coq proof developments and outputing them in the
structured format given in the INRIA technical report RT154. This
program is not for the casual user.

.SH SEE ALSO

.BR coq\-interface (1),
.BR coqc (1),
.BR coqtop (1),
.BR coqdep (1).
.br
.I
The Coq Reference Manual.
.I
The Coq web site: http://coq.inria.fr