Man Linux: Main Page and Category List


       coqtags - creates Proof General tags for coq theories.


       coqtags files


       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
       html format.


       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 <>,
       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