coqtags - creates Proof General tags for coq theories.
This manual page documents the coqtags program. This manual page was
written for the Debian GNU/Linux distribution because the original
program does not have a manual page.
The 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
files One or more theory files for the coq theorem prover. Usually
these files end with .v
This manual page was written by Stefan Schimanski <email@example.com>,
for the Debian GNU/Linux system (but may be used by others).
For more information take a look at the documentation in the info
system with info proofgeneral