aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorErik Martin-Dorel2020-05-06 21:48:52 +0200
committerGitHub2020-05-06 21:48:52 +0200
commitea62543527e6c0fcca8bbb70695e25c2f5d89614 (patch)
tree7677ecfde716f179299d0e8e8475055ac234c868 /doc
parent24e1c5ae3dec16c972babcf44786eb7eff3c6b53 (diff)
parentc3304c49c9d3c1c304e64e34b85ee032b28f3cbe (diff)
Merge pull request #488 from Flupp/doc-info-menu-fix
doc/ProofGeneral.texi: fix makeinfo
Diffstat (limited to 'doc')
-rw-r--r--doc/ProofGeneral.texi1
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 24d4d7e8..dfa09085 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4294,6 +4294,7 @@ assistant. It supports most of the generic features of Proof General.
@menu
* Coq-specific commands::
* Using the Coq project file::
+* Proof using annotations::
* Multiple File Support::
* Editing multiple proofs::
* User-loaded tactics::