diff options
| -rw-r--r-- | doc/ProofGeneral.texi | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 755e009e..03f0644a 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -1936,7 +1936,8 @@ the @code{Search} command of Coq. @c could be generic Coq Proof General provides the program @file{coqtags} to generate tags -for Coq proof scripts. +for Coq proof scripts. Invoking @samp{coqtags *.v} produces a file +@file{TAGS} for all files @samp{*.v} in the current directory. See @ref{Support for tags} for further details on tags. |