diff options
| author | Thomas Kleymann | 1999-02-23 10:26:40 +0000 |
|---|---|---|
| committer | Thomas Kleymann | 1999-02-23 10:26:40 +0000 |
| commit | dbfa2fa4b310f612c47807eeecc6b8ae5f42eaab (patch) | |
| tree | 5b97b93da7743010bb01bb99ef0cd8a73e6b03e8 | |
| parent | a4e5c13a7765eb9b345929a3bbc3e015a4c776ab (diff) | |
extended section on Coq tags
| -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. |