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 COQTAGS 1
.SH NAME
coqtags \- creates Proof General tags for coq theories.
.SH SYNOPSIS
.B coqtags files
.SH "DESCRIPTION"
This manual page documents the
.BR coqtags
program.
This manual page was written for the Debian GNU/Linux distribution
because the original program does not have a manual page.
.PP
The
.B coqtags
command creates a tags table for the specified theory files. Once a tag table
has been made for your proof developments, you can use the Emacs tags mechanisms
to find tags, and complete symbols from tags table.
More information about Proof General tag support can be found in the chapter 5.6
of the Proof General documentation available in info and html format.
.SH OPTIONS
.TP
.B files
One or more theory files for the coq theorem prover. Usually these files end with
.B .v
.
.SH AUTHOR
This manual page was written by Stefan Schimanski <schimmi@debian.org>,
for the Debian GNU/Linux system (but may be used by others).
.SH SEE ALSO
.BR proofgeneral (1)
For more information take a look at the documentation in the info system with
.B info proofgeneral
|
