diff options
| author | David Aspinall | 1999-02-22 14:22:36 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-02-22 14:22:36 +0000 |
| commit | 7039d8b507622f0fda2fe6b72dab2b35c123f9ac (patch) | |
| tree | 8033b9b813a54e6e7d7ed8148f3763c28e686f80 | |
| parent | 995b524cb9a0912be900d24a3bf22e25848f6275 (diff) | |
Coq section on tags improved to mention coqtags.
| -rw-r--r-- | doc/ProofGeneral.texi | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 8bdbe9f0..755e009e 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -1853,12 +1853,13 @@ Refine @node LEGO tags @section LEGO tags -The LEGO Proof General provides the program @file{legotags} to generate -tags for LEGO proof scripts. Invoking @samp{legotags *.l} produces a -file @file{TAGS} for all LEGO modules in the current directory -@footnote{You might want to ask your local system administrator to tag -the directories @file{lib_Prop}, @file{lib_Type} and @file{lib_TYPE} of -the LEGO library.}. +LEGO Proof General provides the program @file{legotags} to generate tags +for LEGO proof scripts. Invoking @samp{legotags *.l} produces a file +@file{TAGS} for all LEGO modules in the current directory @footnote{You +might want to ask your local system administrator to tag the directories +@file{lib_Prop}, @file{lib_Type} and @file{lib_TYPE} of the LEGO +library.}. + See @ref{Support for tags} for further details on tags. @@ -1934,7 +1935,10 @@ the @code{Search} command of Coq. @section Coq tags @c could be generic -Coq tags work as in LEGO, @xref{LEGO tags}. +Coq Proof General provides the program @file{coqtags} to generate tags +for Coq proof scripts. + +See @ref{Support for tags} for further details on tags. @node Editing multiple proofs @section Editing multiple proofs |